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 ( 𝐴 ∈ On ↔ ω ⊆ ( ℵ ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 aleph0 ( ℵ ‘ ∅ ) = ω
2 0ss ∅ ⊆ 𝐴
3 0elon ∅ ∈ On
4 alephord3 ( ( ∅ ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ⊆ 𝐴 ↔ ( ℵ ‘ ∅ ) ⊆ ( ℵ ‘ 𝐴 ) ) )
5 3 4 mpan ( 𝐴 ∈ On → ( ∅ ⊆ 𝐴 ↔ ( ℵ ‘ ∅ ) ⊆ ( ℵ ‘ 𝐴 ) ) )
6 2 5 mpbii ( 𝐴 ∈ On → ( ℵ ‘ ∅ ) ⊆ ( ℵ ‘ 𝐴 ) )
7 1 6 eqsstrrid ( 𝐴 ∈ On → ω ⊆ ( ℵ ‘ 𝐴 ) )
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 ( ¬ 𝐴 ∈ dom ℵ → ( ℵ ‘ 𝐴 ) = ∅ )
16 15 sseq2d ( ¬ 𝐴 ∈ dom ℵ → ( ω ⊆ ( ℵ ‘ 𝐴 ) ↔ ω ⊆ ∅ ) )
17 14 16 mtbiri ( ¬ 𝐴 ∈ dom ℵ → ¬ ω ⊆ ( ℵ ‘ 𝐴 ) )
18 17 con4i ( ω ⊆ ( ℵ ‘ 𝐴 ) → 𝐴 ∈ dom ℵ )
19 alephfnon ℵ Fn On
20 19 fndmi dom ℵ = On
21 18 20 eleqtrdi ( ω ⊆ ( ℵ ‘ 𝐴 ) → 𝐴 ∈ On )
22 7 21 impbii ( 𝐴 ∈ On ↔ ω ⊆ ( ℵ ‘ 𝐴 ) )