c : Cardinal
h : ℵ₀ ≤ c
⊢ ω ≤ alephIdx c
c : Cardinal
h : ℵ₀ ≤ c
⊢ c = aleph (alephIdx c - ω)
rw [aleph, Ordinal.add_sub_cancel_of_le, aleph'_alephIdx]
no goals
c : Cardinal
h : ℵ₀ ≤ c
⊢ ω ≤ alephIdx c
rwa [← aleph0_le_aleph', aleph'_alephIdx]