Metamath Proof Explorer

Theorem alephgeom

Description: Every aleph is greater than or equal to the set of natural numbers. (Contributed by NM, 11-Nov-2003)

Ref Expression
Assertion alephgeom ⊢ A ∈ On ↔ ω ⊆ ℵ ⁡ A

Proof

Step Hyp Ref Expression
1 aleph0 ⊢ ℵ ⁡ ∅ = ω
2 0ss ⊢ ∅ ⊆ A
3 0elon ⊢ ∅ ∈ On
4 alephord3 ⊢ ∅ ∈ On ∧ A ∈ On → ∅ ⊆ A ↔ ℵ ⁡ ∅ ⊆ ℵ ⁡ A
5 3 4 mpan ⊢ A ∈ On → ∅ ⊆ A ↔ ℵ ⁡ ∅ ⊆ ℵ ⁡ A
6 2 5 mpbii ⊢ A ∈ On → ℵ ⁡ ∅ ⊆ ℵ ⁡ A
7 1 6 eqsstrrid ⊢ A ∈ On → ω ⊆ ℵ ⁡ A
8 peano1 ⊢ ∅ ∈ ω
9 ordom ⊢ Ord ⁡ ω
10 ord0 ⊢ Ord ⁡ ∅
11 ordtri1 ⊢ Ord ⁡ ω ∧ Ord ⁡ ∅ → ω ⊆ ∅ ↔ ¬ ∅ ∈ ω
12 9 10 11 mp2an ⊢ ω ⊆ ∅ ↔ ¬ ∅ ∈ ω
13 12 con2bii ⊢ ∅ ∈ ω ↔ ¬ ω ⊆ ∅
14 8 13 mpbi ⊢ ¬ ω ⊆ ∅
15 ndmfv ⊢ ¬ A ∈ dom ⁡ ℵ → ℵ ⁡ A = ∅
16 15 sseq2d ⊢ ¬ A ∈ dom ⁡ ℵ → ω ⊆ ℵ ⁡ A ↔ ω ⊆ ∅
17 14 16 mtbiri ⊢ ¬ A ∈ dom ⁡ ℵ → ¬ ω ⊆ ℵ ⁡ A
18 17 con4i ⊢ ω ⊆ ℵ ⁡ A → A ∈ dom ⁡ ℵ
19 alephfnon ⊢ ℵ Fn On
20 fndm ⊢ ℵ Fn On → dom ⁡ ℵ = On
21 19 20 ax-mp ⊢ dom ⁡ ℵ = On
22 18 21 eleqtrdi ⊢ ω ⊆ ℵ ⁡ A → A ∈ On
23 7 22 impbii ⊢ A ∈ On ↔ ω ⊆ ℵ ⁡ A