α : Type ?u.382418
β : Type ?u.382421
γ : Type ?u.382424
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ ¬bmex o f ∈ range (familyOfBFamily o f)
α : Type ?u.382418
β : Type ?u.382421
γ : Type ?u.382424
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ ¬bmex o f ∈ brange o f
rw [← range_familyOfBFamily]
no goals
α : Type ?u.382418
β : Type ?u.382421
γ : Type ?u.382424
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ ¬bmex o f ∈ range (familyOfBFamily o f)
apply mex_not_mem_range