Metamath Proof Explorer

Theorem pwxpndom

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

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

Proof

Step Hyp Ref Expression
1 pwxpndom2 
 |-  ( _om ~<_ A -> -. ~P A ~<_ ( A |_| ( A X. A ) ) )
2 reldom 
 |-  Rel ~<_
3 2 brrelex2i 
 |-  ( _om ~<_ A -> A e. _V )
4 3 3 xpexd 
 |-  ( _om ~<_ A -> ( A X. A ) e. _V )
5 djudoml 
 |-  ( ( ( A X. A ) e. _V /\ A e. _V ) -> ( A X. A ) ~<_ ( ( A X. A ) |_| A ) )
6 4 3 5 syl2anc 
 |-  ( _om ~<_ A -> ( A X. A ) ~<_ ( ( A X. A ) |_| A ) )
7 djucomen 
 |-  ( ( ( A X. A ) e. _V /\ A e. _V ) -> ( ( A X. A ) |_| A ) ~~ ( A |_| ( A X. A ) ) )
8 4 3 7 syl2anc 
 |-  ( _om ~<_ A -> ( ( A X. A ) |_| A ) ~~ ( A |_| ( A X. A ) ) )
9 domentr 
 |-  ( ( ( A X. A ) ~<_ ( ( A X. A ) |_| A ) /\ ( ( A X. A ) |_| A ) ~~ ( A |_| ( A X. A ) ) ) -> ( A X. A ) ~<_ ( A |_| ( A X. A ) ) )
10 6 8 9 syl2anc 
 |-  ( _om ~<_ A -> ( A X. A ) ~<_ ( A |_| ( A X. A ) ) )
11 domtr 
 |-  ( ( ~P A ~<_ ( A X. A ) /\ ( A X. A ) ~<_ ( A |_| ( A X. A ) ) ) -> ~P A ~<_ ( A |_| ( A X. A ) ) )
12 11 expcom 
 |-  ( ( A X. A ) ~<_ ( A |_| ( A X. A ) ) -> ( ~P A ~<_ ( A X. A ) -> ~P A ~<_ ( A |_| ( A X. A ) ) ) )
13 10 12 syl 
 |-  ( _om ~<_ A -> ( ~P A ~<_ ( A X. A ) -> ~P A ~<_ ( A |_| ( A X. A ) ) ) )
14 1 13 mtod 
 |-  ( _om ~<_ A -> -. ~P A ~<_ ( A X. A ) )