S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
⊢ (∀ (a : Ordinal), enumOrd S a ∈ S) ∧ ∀ (b : Ordinal), b ∈ S → ∃ a, enumOrd S a = b
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
⊢ range (enumOrd S) = S
rw [range_eq_iff]
no goals
S : Set Ordinal
hS : Unbounded (fun x x_1 => x < x_1) S
⊢ (∀ (a : Ordinal), enumOrd S a ∈ S) ∧ ∀ (b : Ordinal), b ∈ S → ∃ a, enumOrd S a = b
exact ⟨enumOrd_mem hS, enumOrd_surjective hS⟩