Metamath Proof Explorer

Theorem pwxpndom2

Description: The powerset of a Dedekind-infinite set does not inject into its Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015) (Proof shortened by AV, 18-Jul-2022)

Ref Expression
Assertion pwxpndom2 
|- ( _om ~<_ A -> -. ~P A ~<_ ( A |_| ( A X. A ) ) )

Proof

Step Hyp Ref Expression
1 pwfseq 
 |-  ( _om ~<_ A -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) )
2 reldom 
 |-  Rel ~<_
3 2 brrelex2i 
 |-  ( _om ~<_ A -> A e. _V )
4 df1o2 
 |-  1o = { (/) }
5 4 oveq2i 
 |-  ( A ^m 1o ) = ( A ^m { (/) } )
6 id 
 |-  ( A e. _V -> A e. _V )
7 0ex 
 |-  (/) e. _V
8 7 a1i 
 |-  ( A e. _V -> (/) e. _V )
9 6 8 mapsnend 
 |-  ( A e. _V -> ( A ^m { (/) } ) ~~ A )
10 5 9 eqbrtrid 
 |-  ( A e. _V -> ( A ^m 1o ) ~~ A )
11 ensym 
 |-  ( ( A ^m 1o ) ~~ A -> A ~~ ( A ^m 1o ) )
12 3 10 11 3syl 
 |-  ( _om ~<_ A -> A ~~ ( A ^m 1o ) )
13 map2xp 
 |-  ( A e. _V -> ( A ^m 2o ) ~~ ( A X. A ) )
14 ensym 
 |-  ( ( A ^m 2o ) ~~ ( A X. A ) -> ( A X. A ) ~~ ( A ^m 2o ) )
15 3 13 14 3syl 
 |-  ( _om ~<_ A -> ( A X. A ) ~~ ( A ^m 2o ) )
16 elmapi 
 |-  ( x e. ( A ^m 1o ) -> x : 1o --> A )
17 16 fdmd 
 |-  ( x e. ( A ^m 1o ) -> dom x = 1o )
18 17 adantr 
 |-  ( ( x e. ( A ^m 1o ) /\ x e. ( A ^m 2o ) ) -> dom x = 1o )
19 1oex 
 |-  1o e. _V
20 19 sucid 
 |-  1o e. suc 1o
21 df-2o 
 |-  2o = suc 1o
22 20 21 eleqtrri 
 |-  1o e. 2o
23 1on 
 |-  1o e. On
24 23 onirri 
 |-  -. 1o e. 1o
25 nelneq2 
 |-  ( ( 1o e. 2o /\ -. 1o e. 1o ) -> -. 2o = 1o )
26 22 24 25 mp2an 
 |-  -. 2o = 1o
27 elmapi 
 |-  ( x e. ( A ^m 2o ) -> x : 2o --> A )
28 27 fdmd 
 |-  ( x e. ( A ^m 2o ) -> dom x = 2o )
29 28 adantl 
 |-  ( ( x e. ( A ^m 1o ) /\ x e. ( A ^m 2o ) ) -> dom x = 2o )
30 29 eqeq1d 
 |-  ( ( x e. ( A ^m 1o ) /\ x e. ( A ^m 2o ) ) -> ( dom x = 1o <-> 2o = 1o ) )
31 26 30 mtbiri 
 |-  ( ( x e. ( A ^m 1o ) /\ x e. ( A ^m 2o ) ) -> -. dom x = 1o )
32 18 31 pm2.65i 
 |-  -. ( x e. ( A ^m 1o ) /\ x e. ( A ^m 2o ) )
33 elin 
 |-  ( x e. ( ( A ^m 1o ) i^i ( A ^m 2o ) ) <-> ( x e. ( A ^m 1o ) /\ x e. ( A ^m 2o ) ) )
34 32 33 mtbir 
 |-  -. x e. ( ( A ^m 1o ) i^i ( A ^m 2o ) )
35 34 a1i 
 |-  ( _om ~<_ A -> -. x e. ( ( A ^m 1o ) i^i ( A ^m 2o ) ) )
36 35 eq0rdv 
 |-  ( _om ~<_ A -> ( ( A ^m 1o ) i^i ( A ^m 2o ) ) = (/) )
37 djuenun 
 |-  ( ( A ~~ ( A ^m 1o ) /\ ( A X. A ) ~~ ( A ^m 2o ) /\ ( ( A ^m 1o ) i^i ( A ^m 2o ) ) = (/) ) -> ( A |_| ( A X. A ) ) ~~ ( ( A ^m 1o ) u. ( A ^m 2o ) ) )
38 12 15 36 37 syl3anc 
 |-  ( _om ~<_ A -> ( A |_| ( A X. A ) ) ~~ ( ( A ^m 1o ) u. ( A ^m 2o ) ) )
39 omex 
 |-  _om e. _V
40 ovex 
 |-  ( A ^m n ) e. _V
41 39 40 iunex 
 |-  U_ n e. _om ( A ^m n ) e. _V
42 1onn 
 |-  1o e. _om
43 oveq2 
 |-  ( n = 1o -> ( A ^m n ) = ( A ^m 1o ) )
44 43 ssiun2s 
 |-  ( 1o e. _om -> ( A ^m 1o ) C_ U_ n e. _om ( A ^m n ) )
45 42 44 ax-mp 
 |-  ( A ^m 1o ) C_ U_ n e. _om ( A ^m n )
46 2onn 
 |-  2o e. _om
47 oveq2 
 |-  ( n = 2o -> ( A ^m n ) = ( A ^m 2o ) )
48 47 ssiun2s 
 |-  ( 2o e. _om -> ( A ^m 2o ) C_ U_ n e. _om ( A ^m n ) )
49 46 48 ax-mp 
 |-  ( A ^m 2o ) C_ U_ n e. _om ( A ^m n )
50 45 49 unssi 
 |-  ( ( A ^m 1o ) u. ( A ^m 2o ) ) C_ U_ n e. _om ( A ^m n )
51 ssdomg 
 |-  ( U_ n e. _om ( A ^m n ) e. _V -> ( ( ( A ^m 1o ) u. ( A ^m 2o ) ) C_ U_ n e. _om ( A ^m n ) -> ( ( A ^m 1o ) u. ( A ^m 2o ) ) ~<_ U_ n e. _om ( A ^m n ) ) )
52 41 50 51 mp2 
 |-  ( ( A ^m 1o ) u. ( A ^m 2o ) ) ~<_ U_ n e. _om ( A ^m n )
53 endomtr 
 |-  ( ( ( A |_| ( A X. A ) ) ~~ ( ( A ^m 1o ) u. ( A ^m 2o ) ) /\ ( ( A ^m 1o ) u. ( A ^m 2o ) ) ~<_ U_ n e. _om ( A ^m n ) ) -> ( A |_| ( A X. A ) ) ~<_ U_ n e. _om ( A ^m n ) )
54 38 52 53 sylancl 
 |-  ( _om ~<_ A -> ( A |_| ( A X. A ) ) ~<_ U_ n e. _om ( A ^m n ) )
55 domtr 
 |-  ( ( ~P A ~<_ ( A |_| ( A X. A ) ) /\ ( A |_| ( A X. A ) ) ~<_ U_ n e. _om ( A ^m n ) ) -> ~P A ~<_ U_ n e. _om ( A ^m n ) )
56 55 expcom 
 |-  ( ( A |_| ( A X. A ) ) ~<_ U_ n e. _om ( A ^m n ) -> ( ~P A ~<_ ( A |_| ( A X. A ) ) -> ~P A ~<_ U_ n e. _om ( A ^m n ) ) )
57 54 56 syl 
 |-  ( _om ~<_ A -> ( ~P A ~<_ ( A |_| ( A X. A ) ) -> ~P A ~<_ U_ n e. _om ( A ^m n ) ) )
58 1 57 mtod 
 |-  ( _om ~<_ A -> -. ~P A ~<_ ( A |_| ( A X. A ) ) )