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