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 ⊢ℵFnOn
20 19 fndmi ⊢dom⁡ℵ=On
21 18 20 eleqtrdi ⊢ω⊆ℵ⁡A→A∈On
22 7 21 impbii ⊢A∈On↔ω⊆ℵ⁡A