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 
|- ( 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 ) )