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 e. On <-> _om C_ ( aleph ` A ) )

Proof

Step Hyp Ref Expression
1 aleph0
 |-  ( aleph ` (/) ) = _om
2 0ss
 |-  (/) C_ A
3 0elon
 |-  (/) e. On
4 alephord3
 |-  ( ( (/) e. On /\ A e. On ) -> ( (/) C_ A <-> ( aleph ` (/) ) C_ ( aleph ` A ) ) )
5 3 4 mpan
 |-  ( A e. On -> ( (/) C_ A <-> ( aleph ` (/) ) C_ ( aleph ` A ) ) )
6 2 5 mpbii
 |-  ( A e. On -> ( aleph ` (/) ) C_ ( aleph ` A ) )
7 1 6 eqsstrrid
 |-  ( A e. On -> _om C_ ( aleph ` A ) )
8 peano1
 |-  (/) e. _om
9 ordom
 |-  Ord _om
10 ord0
 |-  Ord (/)
11 ordtri1
 |-  ( ( Ord _om /\ Ord (/) ) -> ( _om C_ (/) <-> -. (/) e. _om ) )
12 9 10 11 mp2an
 |-  ( _om C_ (/) <-> -. (/) e. _om )
13 12 con2bii
 |-  ( (/) e. _om <-> -. _om C_ (/) )
14 8 13 mpbi
 |-  -. _om C_ (/)
15 ndmfv
 |-  ( -. A e. dom aleph -> ( aleph ` A ) = (/) )
16 15 sseq2d
 |-  ( -. A e. dom aleph -> ( _om C_ ( aleph ` A ) <-> _om C_ (/) ) )
17 14 16 mtbiri
 |-  ( -. A e. dom aleph -> -. _om C_ ( aleph ` A ) )
18 17 con4i
 |-  ( _om C_ ( aleph ` A ) -> A e. dom aleph )
19 alephfnon
 |-  aleph Fn On
20 19 fndmi
 |-  dom aleph = On
21 18 20 eleqtrdi
 |-  ( _om C_ ( aleph ` A ) -> A e. On )
22 7 21 impbii
 |-  ( A e. On <-> _om C_ ( aleph ` A ) )