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