ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
s : Set Ordinal
x✝ : s ∈ Set.range fun i => fixedPoints (f i)
i : ι
hi : (fun i => fixedPoints (f i)) i = s
⊢ f i (nfpFamily f a) = nfpFamily f a
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
s : Set Ordinal
x✝ : s ∈ Set.range fun i => fixedPoints (f i)
i : ι
hi : (fun i => fixedPoints (f i)) i = s
⊢ nfpFamily f a ∈ s
rw [← hi, mem_fixedPoints_iff]
no goals
ι : Type u
f : ι → Ordinal → Ordinal
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal
s : Set Ordinal
x✝ : s ∈ Set.range fun i => fixedPoints (f i)
i : ι
hi : (fun i => fixedPoints (f i)) i = s
⊢ f i (nfpFamily f a) = nfpFamily f a
exact nfpFamily_fp.{u, v} (H i) a