c : Cardinal
⊢ (∀ (o' : Ordinal) (x : ℕ), o' = ↑x → aleph' o' ≤ c) ↔ ∀ (n : ℕ), ↑n ≤ c
c : Cardinal
⊢ aleph' ω ≤ c ↔ ℵ₀ ≤ c
simp only [aleph'_le_of_limit omega_isLimit, lt_omega, exists_imp, aleph0_le]
no goals
c : Cardinal
⊢ (∀ (o' : Ordinal) (x : ℕ), o' = ↑x → aleph' o' ≤ c) ↔ ∀ (n : ℕ), ↑n ≤ c
exact forall_swap.trans (forall_congr' fun n => by simp only [forall_eq, aleph'_nat])
no goals
c : Cardinal
n : ℕ
⊢ (∀ (x : Ordinal), x = ↑n → aleph' x ≤ c) ↔ ↑n ≤ c
simp only [forall_eq, aleph'_nat]