no goals
α : Type ?u.279751
β : Type ?u.279754
γ : Type ?u.279757
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
a : Ordinal
⊢ (∀ (x : Ordinal), x ∈ range f → x ≤ a) ↔ ∀ (i : ι), f i ≤ a
simp