o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
⊢ ∀ (i : Ordinal) (j : i < o), nfpBFamily o f a ∈ fixedPoints (f i j)
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
⊢ nfpBFamily o f a ∈ ⋂ (i : Ordinal) (hi : i < o), fixedPoints (f i hi)
rw [Set.mem_iInter₂]
no goals
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
⊢ ∀ (i : Ordinal) (j : i < o), nfpBFamily o f a ∈ fixedPoints (f i j)
exact fun i hi => nfpBFamily_fp (H i hi) _