This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gchdjuidm

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

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> A e. GCH )
2 djudoml 
 |-  ( ( A e. GCH /\ A e. GCH ) -> A ~<_ ( A |_| A ) )
3 1 1 2 syl2anc 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> A ~<_ ( A |_| A ) )
4 canth2g 
 |-  ( A e. GCH -> A ~< ~P A )
5 4 adantr 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> A ~< ~P A )
6 sdomdom 
 |-  ( A ~< ~P A -> A ~<_ ~P A )
7 5 6 syl 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> A ~<_ ~P A )
8 reldom 
 |-  Rel ~<_
9 8 brrelex1i 
 |-  ( A ~<_ ~P A -> A e. _V )
10 djudom1 
 |-  ( ( A ~<_ ~P A /\ A e. _V ) -> ( A |_| A ) ~<_ ( ~P A |_| A ) )
11 9 10 mpdan 
 |-  ( A ~<_ ~P A -> ( A |_| A ) ~<_ ( ~P A |_| A ) )
12 9 pwexd 
 |-  ( A ~<_ ~P A -> ~P A e. _V )
13 djudom2 
 |-  ( ( A ~<_ ~P A /\ ~P A e. _V ) -> ( ~P A |_| A ) ~<_ ( ~P A |_| ~P A ) )
14 12 13 mpdan 
 |-  ( A ~<_ ~P A -> ( ~P A |_| A ) ~<_ ( ~P A |_| ~P A ) )
15 domtr 
 |-  ( ( ( A |_| A ) ~<_ ( ~P A |_| A ) /\ ( ~P A |_| A ) ~<_ ( ~P A |_| ~P A ) ) -> ( A |_| A ) ~<_ ( ~P A |_| ~P A ) )
16 11 14 15 syl2anc 
 |-  ( A ~<_ ~P A -> ( A |_| A ) ~<_ ( ~P A |_| ~P A ) )
17 7 16 syl 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A |_| A ) ~<_ ( ~P A |_| ~P A ) )
18 pwdju1 
 |-  ( A e. GCH -> ( ~P A |_| ~P A ) ~~ ~P ( A |_| 1o ) )
19 18 adantr 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( ~P A |_| ~P A ) ~~ ~P ( A |_| 1o ) )
20 gchdju1 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A |_| 1o ) ~~ A )
21 pwen 
 |-  ( ( A |_| 1o ) ~~ A -> ~P ( A |_| 1o ) ~~ ~P A )
22 20 21 syl 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ~P ( A |_| 1o ) ~~ ~P A )
23 entr 
 |-  ( ( ( ~P A |_| ~P A ) ~~ ~P ( A |_| 1o ) /\ ~P ( A |_| 1o ) ~~ ~P A ) -> ( ~P A |_| ~P A ) ~~ ~P A )
24 19 22 23 syl2anc 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( ~P A |_| ~P A ) ~~ ~P A )
25 domentr 
 |-  ( ( ( A |_| A ) ~<_ ( ~P A |_| ~P A ) /\ ( ~P A |_| ~P A ) ~~ ~P A ) -> ( A |_| A ) ~<_ ~P A )
26 17 24 25 syl2anc 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A |_| A ) ~<_ ~P A )
27 gchinf 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> _om ~<_ A )
28 pwdjundom 
 |-  ( _om ~<_ A -> -. ~P A ~<_ ( A |_| A ) )
29 27 28 syl 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> -. ~P A ~<_ ( A |_| A ) )
30 ensym 
 |-  ( ( A |_| A ) ~~ ~P A -> ~P A ~~ ( A |_| A ) )
31 endom 
 |-  ( ~P A ~~ ( A |_| A ) -> ~P A ~<_ ( A |_| A ) )
32 30 31 syl 
 |-  ( ( A |_| A ) ~~ ~P A -> ~P A ~<_ ( A |_| A ) )
33 29 32 nsyl 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> -. ( A |_| A ) ~~ ~P A )
34 brsdom 
 |-  ( ( A |_| A ) ~< ~P A <-> ( ( A |_| A ) ~<_ ~P A /\ -. ( A |_| A ) ~~ ~P A ) )
35 26 33 34 sylanbrc 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A |_| A ) ~< ~P A )
36 3 35 jca 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A ~<_ ( A |_| A ) /\ ( A |_| A ) ~< ~P A ) )
37 gchen1 
 |-  ( ( ( A e. GCH /\ -. A e. Fin ) /\ ( A ~<_ ( A |_| A ) /\ ( A |_| A ) ~< ~P A ) ) -> A ~~ ( A |_| A ) )
38 36 37 mpdan 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> A ~~ ( A |_| A ) )
39 38 ensymd 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A |_| A ) ~~ A )