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	⊢ ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		pwxpndom2	⊢ ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )
2		df1o2	⊢ 1o = { ∅ }
3	2	xpeq1i	⊢ ( 1o × 𝐴 ) = ( { ∅ } × 𝐴 )
4		0ex	⊢ ∅ ∈ V
5		reldom	⊢ Rel ≼
6	5	brrelex2i	⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
7		xpsnen2g	⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ V ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
8	4 6 7	sylancr	⊢ ( ω ≼ 𝐴 → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
9	3 8	eqbrtrid	⊢ ( ω ≼ 𝐴 → ( 1o × 𝐴 ) ≈ 𝐴 )
10	9	ensymd	⊢ ( ω ≼ 𝐴 → 𝐴 ≈ ( 1o × 𝐴 ) )
11		omex	⊢ ω ∈ V
12		ordom	⊢ Ord ω
13		1onn	⊢ 1o ∈ ω
14		ordelss	⊢ ( ( Ord ω ∧ 1o ∈ ω ) → 1o ⊆ ω )
15	12 13 14	mp2an	⊢ 1o ⊆ ω
16		ssdomg	⊢ ( ω ∈ V → ( 1o ⊆ ω → 1o ≼ ω ) )
17	11 15 16	mp2	⊢ 1o ≼ ω
18		domtr	⊢ ( ( 1o ≼ ω ∧ ω ≼ 𝐴 ) → 1o ≼ 𝐴 )
19	17 18	mpan	⊢ ( ω ≼ 𝐴 → 1o ≼ 𝐴 )
20		xpdom1g	⊢ ( ( 𝐴 ∈ V ∧ 1o ≼ 𝐴 ) → ( 1o × 𝐴 ) ≼ ( 𝐴 × 𝐴 ) )
21	6 19 20	syl2anc	⊢ ( ω ≼ 𝐴 → ( 1o × 𝐴 ) ≼ ( 𝐴 × 𝐴 ) )
22		endomtr	⊢ ( ( 𝐴 ≈ ( 1o × 𝐴 ) ∧ ( 1o × 𝐴 ) ≼ ( 𝐴 × 𝐴 ) ) → 𝐴 ≼ ( 𝐴 × 𝐴 ) )
23	10 21 22	syl2anc	⊢ ( ω ≼ 𝐴 → 𝐴 ≼ ( 𝐴 × 𝐴 ) )
24		djudom2	⊢ ( ( 𝐴 ≼ ( 𝐴 × 𝐴 ) ∧ 𝐴 ∈ V ) → ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )
25	23 6 24	syl2anc	⊢ ( ω ≼ 𝐴 → ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )
26		domtr	⊢ ( ( 𝒫 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) ∧ ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ) → 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )
27	26	expcom	⊢ ( ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) → ( 𝒫 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) → 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ) )
28	25 27	syl	⊢ ( ω ≼ 𝐴 → ( 𝒫 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) → 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ) )
29	1 28	mtod	⊢ ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) )