α : Type ?u.312340
β : Type ?u.312343
γ : Type ?u.312346
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ {i : Ordinal} (h : i < o), f i h ≠ sup (familyOfBFamily o f)
a : Ordinal
⊢ a < sup (familyOfBFamily o f) → succ a < sup (familyOfBFamily o f)
α : Type ?u.312340
β : Type ?u.312343
γ : Type ?u.312346
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ {i : Ordinal} (h : i < o), f i h ≠ bsup o f
a : Ordinal
⊢ a < bsup o f → succ a < bsup o f
rw [← sup_eq_bsup] at *
no goals
α : Type ?u.312340
β : Type ?u.312343
γ : Type ?u.312346
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ {i : Ordinal} (h : i < o), f i h ≠ sup (familyOfBFamily o f)
a : Ordinal
⊢ a < sup (familyOfBFamily o f) → succ a < sup (familyOfBFamily o f)
exact sup_not_succ_of_ne_sup fun i => hf _