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 ) ) )