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 0fin
 |-  (/) 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 )