Theorem aleph1 5019

Description: The set exponentiation of 2 to the aleph-zero has cardinality of at least aleph-one. (If we were to assume the Continuum Hypothesis, their cardinalities would be the same.)

Assertion

Ref	Expression
aleph1	|- (aleph` 1o) ~<_ (2o ^m (aleph` (/)))

Proof of Theorem aleph1

Step	Hyp	Ref	Expression
1		df-1o 4267	. . 3 |- 1o = suc (/)
2	1	fveq2i 3837	. 2 |- (aleph` 1o) = (aleph` suc (/))
3		alephsucpw 5018	. . 3 |- (aleph` suc (/)) ~<_ P~(aleph` (/))
4		oprex 4039	. . . 4 |- (2o ^m (aleph` (/))) e. V
5		fvex 3842	. . . . 5 |- (aleph` (/)) e. V
6	5	pw2en 4585	. . . 4 |- P~(aleph` (/)) ~~ (2o ^m (aleph` (/)))
7		domen2 4623	. . . 4 |- (((2o ^m (aleph` (/))) e. V /\ P~(aleph` (/)) ~~ (2o ^m (aleph` (/)))) -> ((aleph` suc (/)) ~<_ P~(aleph` (/)) <-> (aleph` suc (/)) ~<_ (2o ^m (aleph` (/)))))
8	4, 6, 7	mp2an 700	. . 3 |- ((aleph` suc (/)) ~<_ P~(aleph` (/)) <-> (aleph` suc (/)) ~<_ (2o ^m (aleph` (/))))
9	3, 8	mpbi 187	. 2 |- (aleph` suc (/)) ~<_ (2o ^m (aleph` (/)))
10	2, 9	eqbrtri 2706	1 |- (aleph` 1o) ~<_ (2o ^m (aleph` (/)))

Syntax hints:   <-> wb 144   e. wcel 993  Vcvv 1856  (/)c0 2331  P~cpw 2457   class class class wbr 2691  suc csuc 2976  ` cfv 3262  (class class class)co 4019  1oc1o 4262  2oc2o 4263   ^m cm 4461   ~~ cen 4503   ~<_ cdom 4504  alephcale 4958

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 997  ax-gen 998  ax-8 999  ax-9 1000  ax-10 1001  ax-11 1002  ax-12 1003  ax-13 1004  ax-14 1005  ax-17 1006  ax-4 1008  ax-5o 1010  ax-6o 1013  ax-9o 1158  ax-10o 1176  ax-16 1246  ax-11o 1254  ax-ext 1499  ax-rep 2766  ax-sep 2776  ax-nul 2783  ax-pow 2817  ax-pr 2854  ax-un 3088  ax-reg 4734  ax-inf2 4768  ax-ac 4888

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 781  df-3an 782  df-ex 1016  df-sb 1208  df-eu 1420  df-mo 1421  df-clab 1505  df-cleq 1510  df-clel 1513  df-ne 1629  df-ral 1694  df-rex 1695  df-reu 1696  df-rab 1697  df-v 1857  df-sbc 1986  df-csb 2051  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-pss 2106  df-nul 2332  df-if 2415  df-pw 2458  df-sn 2469  df-pr 2470  df-tp 2472  df-op 2473  df-uni 2569  df-int 2600  df-iun 2634  df-br 2692  df-opab 2740  df-tr 2754  df-eprel 2909  df-id 2912  df-po 2917  df-so 2928  df-fr 2946  df-we 2961  df-ord 2977  df-on 2978  df-lim 2979  df-suc 2980  df-om 3218  df-xp 3264  df-rel 3265  df-cnv 3266  df-co 3267  df-dm 3268  df-rn 3269  df-res 3270  df-ima 3271  df-fun 3272  df-fn 3273  df-f 3274  df-f1 3275  df-fo 3276  df-f1o 3277  df-fv 3278  df-opr 4021  df-oprab 4022  df-rdg 4231  df-1o 4267  df-2o 4268  df-er 4399  df-map 4463  df-en 4507  df-dom 4508  df-sdom 4509  df-fin 4510  df-card 4960  df-aleph 4961

Copyright terms: Public domain