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

Metamath Proof Explorer

Theorem pwdjundom

Description: The powerset of a Dedekind-infinite set does not inject into its cardinal sum with itself. (Contributed by Mario Carneiro, 31-May-2015)

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

Proof

Step Hyp Ref Expression
1 pwxpndom2 
 |-  ( _om ~<_ A -> -. ~P A ~<_ ( A |_| ( A X. A ) ) )
2 df1o2 
 |-  1o = { (/) }
3 2 xpeq1i 
 |-  ( 1o X. A ) = ( { (/) } X. A )
4 0ex 
 |-  (/) e. _V
5 reldom 
 |-  Rel ~<_
6 5 brrelex2i 
 |-  ( _om ~<_ A -> A e. _V )
7 xpsnen2g 
 |-  ( ( (/) e. _V /\ A e. _V ) -> ( { (/) } X. A ) ~~ A )
8 4 6 7 sylancr 
 |-  ( _om ~<_ A -> ( { (/) } X. A ) ~~ A )
9 3 8 eqbrtrid 
 |-  ( _om ~<_ A -> ( 1o X. A ) ~~ A )
10 9 ensymd 
 |-  ( _om ~<_ A -> A ~~ ( 1o X. A ) )
11 omex 
 |-  _om e. _V
12 ordom 
 |-  Ord _om
13 1onn 
 |-  1o e. _om
14 ordelss 
 |-  ( ( Ord _om /\ 1o e. _om ) -> 1o C_ _om )
15 12 13 14 mp2an 
 |-  1o C_ _om
16 ssdomg 
 |-  ( _om e. _V -> ( 1o C_ _om -> 1o ~<_ _om ) )
17 11 15 16 mp2 
 |-  1o ~<_ _om
18 domtr 
 |-  ( ( 1o ~<_ _om /\ _om ~<_ A ) -> 1o ~<_ A )
19 17 18 mpan 
 |-  ( _om ~<_ A -> 1o ~<_ A )
20 xpdom1g 
 |-  ( ( A e. _V /\ 1o ~<_ A ) -> ( 1o X. A ) ~<_ ( A X. A ) )
21 6 19 20 syl2anc 
 |-  ( _om ~<_ A -> ( 1o X. A ) ~<_ ( A X. A ) )
22 endomtr 
 |-  ( ( A ~~ ( 1o X. A ) /\ ( 1o X. A ) ~<_ ( A X. A ) ) -> A ~<_ ( A X. A ) )
23 10 21 22 syl2anc 
 |-  ( _om ~<_ A -> A ~<_ ( A X. A ) )
24 djudom2 
 |-  ( ( A ~<_ ( A X. A ) /\ A e. _V ) -> ( A |_| A ) ~<_ ( A |_| ( A X. A ) ) )
25 23 6 24 syl2anc 
 |-  ( _om ~<_ A -> ( A |_| A ) ~<_ ( A |_| ( A X. A ) ) )
26 domtr 
 |-  ( ( ~P A ~<_ ( A |_| A ) /\ ( A |_| A ) ~<_ ( A |_| ( A X. A ) ) ) -> ~P A ~<_ ( A |_| ( A X. A ) ) )
27 26 expcom 
 |-  ( ( A |_| A ) ~<_ ( A |_| ( A X. A ) ) -> ( ~P A ~<_ ( A |_| A ) -> ~P A ~<_ ( A |_| ( A X. A ) ) ) )
28 25 27 syl 
 |-  ( _om ~<_ A -> ( ~P A ~<_ ( A |_| A ) -> ~P A ~<_ ( A |_| ( A X. A ) ) ) )
29 1 28 mtod 
 |-  ( _om ~<_ A -> -. ~P A ~<_ ( A |_| A ) )