α : Type ?u.388950
β : Type ?u.388953
γ : Type ?u.388956
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ bmex o f < ord (succ (#(Quotient.out o).α))
α : Type ?u.388950
β : Type ?u.388953
γ : Type ?u.388956
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ bmex o f < ord (succ (card o))
rw [← mk_ordinal_out]
no goals
α : Type ?u.388950
β : Type ?u.388953
γ : Type ?u.388956
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ bmex o f < ord (succ (#(Quotient.out o).α))
exact mex_lt_ord_succ_mk (familyOfBFamily o f)