MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gchpwdom Unicode version

Theorem gchpwdom 9069
Description: A relationship between dominance over the powerset and strict dominance when the sets involved are infinite GCH-sets. Proposition 3.1 of [KanamoriPincus] p. 421. (Contributed by Mario Carneiro, 31-May-2015.)
Assertion
Ref Expression
gchpwdom

Proof of Theorem gchpwdom
StepHypRef Expression
1 simpl2 1000 . . . . . . 7
2 pwexg 4636 . . . . . . 7
31, 2syl 16 . . . . . 6
4 simpl3 1001 . . . . . 6
5 cdadom3 8589 . . . . . 6
63, 4, 5syl2anc 661 . . . . 5
7 domen2 7680 . . . . 5
86, 7syl5ibrcom 222 . . . 4
9 cdacomen 8582 . . . . . . 7
10 entr 7587 . . . . . . 7
119, 10mpan 670 . . . . . 6
12 ensym 7584 . . . . . 6
13 endom 7562 . . . . . 6
1411, 12, 133syl 20 . . . . 5
15 domsdomtr 7672 . . . . . . . . . . 11
16153ad2antl1 1158 . . . . . . . . . 10
17 sdomnsym 7662 . . . . . . . . . 10
1816, 17syl 16 . . . . . . . . 9
19 isfinite 8090 . . . . . . . . 9
2018, 19sylnibr 305 . . . . . . . 8
21 gchcdaidm 9067 . . . . . . . 8
224, 20, 21syl2anc 661 . . . . . . 7
23 pwen 7710 . . . . . . 7
24 domen1 7679 . . . . . . 7
2522, 23, 243syl 20 . . . . . 6
26 pwcdadom 8617 . . . . . . 7
27 canth2g 7691 . . . . . . . . 9
28 sdomdomtr 7670 . . . . . . . . . 10
2928ex 434 . . . . . . . . 9
304, 27, 293syl 20 . . . . . . . 8
31 gchi 9023 . . . . . . . . . 10
32313expia 1198 . . . . . . . . 9
33323ad2antl2 1159 . . . . . . . 8
34 isfinite 8090 . . . . . . . . 9
35 simpl1 999 . . . . . . . . . . 11
36 domnsym 7663 . . . . . . . . . . 11
3735, 36syl 16 . . . . . . . . . 10
3837pm2.21d 106 . . . . . . . . 9
3934, 38syl5bi 217 . . . . . . . 8
4030, 33, 393syld 55 . . . . . . 7
4126, 40syl5 32 . . . . . 6
4225, 41sylbird 235 . . . . 5
4314, 42syl5 32 . . . 4
44 cdadom3 8589 . . . . . . 7
454, 3, 44syl2anc 661 . . . . . 6
46 domentr 7594 . . . . . 6
4745, 9, 46sylancl 662 . . . . 5
48 sdomdom 7563 . . . . . . . . 9
4948adantl 466 . . . . . . . 8
50 pwdom 7689 . . . . . . . 8
51 cdadom1 8587 . . . . . . . 8
5249, 50, 513syl 20 . . . . . . 7
534, 27syl 16 . . . . . . . 8
54 sdomdom 7563 . . . . . . . 8
55 cdadom2 8588 . . . . . . . 8
5653, 54, 553syl 20 . . . . . . 7
57 domtr 7588 . . . . . . 7
5852, 56, 57syl2anc 661 . . . . . 6
59 pwcda1 8595 . . . . . . . 8
604, 59syl 16 . . . . . . 7
61 gchcda1 9055 . . . . . . . . 9
624, 20, 61syl2anc 661 . . . . . . . 8
63 pwen 7710 . . . . . . . 8
6462, 63syl 16 . . . . . . 7
65 entr 7587 . . . . . . 7
6660, 64, 65syl2anc 661 . . . . . 6
67 domentr 7594 . . . . . 6
6858, 66, 67syl2anc 661 . . . . 5
69 gchor 9026 . . . . 5
704, 20, 47, 68, 69syl22anc 1229 . . . 4
718, 43, 70mpjaod 381 . . 3
7271ex 434 . 2
73 reldom 7542 . . . . 5
7473brrelexi 5045 . . . 4
75 pwexb 6611 . . . . 5
76 canth2g 7691 . . . . 5
7775, 76sylbir 213 . . . 4
7874, 77syl 16 . . 3
79 sdomdomtr 7670 . . 3
8078, 79mpancom 669 . 2
8172, 80impbid1 203 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  /\w3a 973  e.wcel 1818   cvv 3109  ~Pcpw 4012   class class class wbr 4452  (class class class)co 6296   com 6700   c1o 7142   cen 7533   cdom 7534   csdm 7535   cfn 7536   ccda 8568   cgch 9019
This theorem is referenced by:  gchaleph2  9071  gchina  9098
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-inf2 8079
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-fal 1401  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-int 4287  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-se 4844  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-isom 5602  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-1st 6800  df-2nd 6801  df-supp 6919  df-recs 7061  df-rdg 7095  df-seqom 7132  df-1o 7149  df-2o 7150  df-oadd 7153  df-omul 7154  df-oexp 7155  df-er 7330  df-map 7441  df-en 7537  df-dom 7538  df-sdom 7539  df-fin 7540  df-fsupp 7850  df-oi 7956  df-har 8005  df-wdom 8006  df-cnf 8100  df-card 8341  df-cda 8569  df-fin4 8688  df-gch 9020
  Copyright terms: Public domain W3C validator