This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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