S : Set Ordinal
⊢ sInf (S ∩ {b | ∀ (c : Ordinal), c < 0 → enumOrd S c < b}) = sInf S
S : Set Ordinal
⊢ enumOrd S 0 = sInf S
rw [enumOrd_def]
no goals
S : Set Ordinal
⊢ sInf (S ∩ {b | ∀ (c : Ordinal), c < 0 → enumOrd S c < b}) = sInf S
simp [Ordinal.not_lt_zero]