S : Set Ordinal
o : Ordinal
⊢ sInf (S ∩ Ici (blsub o fun a x => enumOrd S a)) = sInf (S ∩ {b | ∀ (c : Ordinal), c < o → enumOrd S c < b})
S : Set Ordinal
o : Ordinal
⊢ enumOrd S o = sInf (S ∩ {b | ∀ (c : Ordinal), c < o → enumOrd S c < b})
rw [enumOrd_def']
case e_a.e_a
S : Set Ordinal
o : Ordinal
⊢ Ici (blsub o fun a x => enumOrd S a) = {b | ∀ (c : Ordinal), c < o → enumOrd S c < b}
S : Set Ordinal
o : Ordinal
⊢ sInf (S ∩ Ici (blsub o fun a x => enumOrd S a)) = sInf (S ∩ {b | ∀ (c : Ordinal), c < o → enumOrd S c < b})
congr
case e_a.e_a.h
S : Set Ordinal
o x✝ : Ordinal
⊢ x✝ ∈ Ici (blsub o fun a x => enumOrd S a) ↔ x✝ ∈ {b | ∀ (c : Ordinal), c < o → enumOrd S c < b}
case e_a.e_a
S : Set Ordinal
o : Ordinal
⊢ Ici (blsub o fun a x => enumOrd S a) = {b | ∀ (c : Ordinal), c < o → enumOrd S c < b}
ext
no goals
case e_a.e_a.h
S : Set Ordinal
o x✝ : Ordinal
⊢ x✝ ∈ Ici (blsub o fun a x => enumOrd S a) ↔ x✝ ∈ {b | ∀ (c : Ordinal), c < o → enumOrd S c < b}
exact ⟨fun h a hao => (lt_blsub.{u, u} _ _ hao).trans_le h, blsub_le⟩