Metamath Proof Explorer

Theorem gchxpidm

Description: An infinite GCH-set is idempotent under cardinal product. Part of Lemma 2.2 of KanamoriPincus p. 419. (Contributed by Mario Carneiro, 31-May-2015)

Ref Expression
Assertion gchxpidm 
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. A ) ~~ A )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 1 a1i 
 |-  ( -. A e. Fin -> (/) e. _V )
3 xpsneng 
 |-  ( ( A e. GCH /\ (/) e. _V ) -> ( A X. { (/) } ) ~~ A )
4 2 3 sylan2 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. { (/) } ) ~~ A )
5 4 ensymd 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> A ~~ ( A X. { (/) } ) )
6 df1o2 
 |-  1o = { (/) }
7 id 
 |-  ( A = (/) -> A = (/) )
8 0fi 
 |-  (/) e. Fin
9 7 8 eqeltrdi 
 |-  ( A = (/) -> A e. Fin )
10 9 necon3bi 
 |-  ( -. A e. Fin -> A =/= (/) )
11 10 adantl 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> A =/= (/) )
12 0sdomg 
 |-  ( A e. GCH -> ( (/) ~< A <-> A =/= (/) ) )
13 12 adantr 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( (/) ~< A <-> A =/= (/) ) )
14 11 13 mpbird 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> (/) ~< A )
15 0sdom1dom 
 |-  ( (/) ~< A <-> 1o ~<_ A )
16 14 15 sylib 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> 1o ~<_ A )
17 6 16 eqbrtrrid 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> { (/) } ~<_ A )
18 xpdom2g 
 |-  ( ( A e. GCH /\ { (/) } ~<_ A ) -> ( A X. { (/) } ) ~<_ ( A X. A ) )
19 17 18 syldan 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. { (/) } ) ~<_ ( A X. A ) )
20 endomtr 
 |-  ( ( A ~~ ( A X. { (/) } ) /\ ( A X. { (/) } ) ~<_ ( A X. A ) ) -> A ~<_ ( A X. A ) )
21 5 19 20 syl2anc 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> A ~<_ ( A X. A ) )
22 canth2g 
 |-  ( A e. GCH -> A ~< ~P A )
23 22 adantr 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> A ~< ~P A )
24 sdomdom 
 |-  ( A ~< ~P A -> A ~<_ ~P A )
25 23 24 syl 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> A ~<_ ~P A )
26 xpdom1g 
 |-  ( ( A e. GCH /\ A ~<_ ~P A ) -> ( A X. A ) ~<_ ( ~P A X. A ) )
27 25 26 syldan 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. A ) ~<_ ( ~P A X. A ) )
28 pwexg 
 |-  ( A e. GCH -> ~P A e. _V )
29 28 adantr 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ~P A e. _V )
30 xpdom2g 
 |-  ( ( ~P A e. _V /\ A ~<_ ~P A ) -> ( ~P A X. A ) ~<_ ( ~P A X. ~P A ) )
31 29 25 30 syl2anc 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( ~P A X. A ) ~<_ ( ~P A X. ~P A ) )
32 domtr 
 |-  ( ( ( A X. A ) ~<_ ( ~P A X. A ) /\ ( ~P A X. A ) ~<_ ( ~P A X. ~P A ) ) -> ( A X. A ) ~<_ ( ~P A X. ~P A ) )
33 27 31 32 syl2anc 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. A ) ~<_ ( ~P A X. ~P A ) )
34 simpl 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> A e. GCH )
35 pwdjuen 
 |-  ( ( A e. GCH /\ A e. GCH ) -> ~P ( A |_| A ) ~~ ( ~P A X. ~P A ) )
36 34 35 syldan 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ~P ( A |_| A ) ~~ ( ~P A X. ~P A ) )
37 36 ensymd 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( ~P A X. ~P A ) ~~ ~P ( A |_| A ) )
38 gchdjuidm 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A |_| A ) ~~ A )
39 pwen 
 |-  ( ( A |_| A ) ~~ A -> ~P ( A |_| A ) ~~ ~P A )
40 38 39 syl 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ~P ( A |_| A ) ~~ ~P A )
41 entr 
 |-  ( ( ( ~P A X. ~P A ) ~~ ~P ( A |_| A ) /\ ~P ( A |_| A ) ~~ ~P A ) -> ( ~P A X. ~P A ) ~~ ~P A )
42 37 40 41 syl2anc 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( ~P A X. ~P A ) ~~ ~P A )
43 domentr 
 |-  ( ( ( A X. A ) ~<_ ( ~P A X. ~P A ) /\ ( ~P A X. ~P A ) ~~ ~P A ) -> ( A X. A ) ~<_ ~P A )
44 33 42 43 syl2anc 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. A ) ~<_ ~P A )
45 gchinf 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> _om ~<_ A )
46 pwxpndom 
 |-  ( _om ~<_ A -> -. ~P A ~<_ ( A X. A ) )
47 45 46 syl 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> -. ~P A ~<_ ( A X. A ) )
48 ensym 
 |-  ( ( A X. A ) ~~ ~P A -> ~P A ~~ ( A X. A ) )
49 endom 
 |-  ( ~P A ~~ ( A X. A ) -> ~P A ~<_ ( A X. A ) )
50 48 49 syl 
 |-  ( ( A X. A ) ~~ ~P A -> ~P A ~<_ ( A X. A ) )
51 47 50 nsyl 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> -. ( A X. A ) ~~ ~P A )
52 brsdom 
 |-  ( ( A X. A ) ~< ~P A <-> ( ( A X. A ) ~<_ ~P A /\ -. ( A X. A ) ~~ ~P A ) )
53 44 51 52 sylanbrc 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. A ) ~< ~P A )
54 21 53 jca 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A ~<_ ( A X. A ) /\ ( A X. A ) ~< ~P A ) )
55 gchen1 
 |-  ( ( ( A e. GCH /\ -. A e. Fin ) /\ ( A ~<_ ( A X. A ) /\ ( A X. A ) ~< ~P A ) ) -> A ~~ ( A X. A ) )
56 54 55 mpdan 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> A ~~ ( A X. A ) )
57 56 ensymd 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. A ) ~~ A )