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

Proof

Step	Hyp	Ref	Expression
1		pwxpndom2	⊢ ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )
2		reldom	⊢ Rel ≼
3	2	brrelex2i	⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
4	3 3	xpexd	⊢ ( ω ≼ 𝐴 → ( 𝐴 × 𝐴 ) ∈ V )
5		djudoml	⊢ ( ( ( 𝐴 × 𝐴 ) ∈ V ∧ 𝐴 ∈ V ) → ( 𝐴 × 𝐴 ) ≼ ( ( 𝐴 × 𝐴 ) ⊔ 𝐴 ) )
6	4 3 5	syl2anc	⊢ ( ω ≼ 𝐴 → ( 𝐴 × 𝐴 ) ≼ ( ( 𝐴 × 𝐴 ) ⊔ 𝐴 ) )
7		djucomen	⊢ ( ( ( 𝐴 × 𝐴 ) ∈ V ∧ 𝐴 ∈ V ) → ( ( 𝐴 × 𝐴 ) ⊔ 𝐴 ) ≈ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )
8	4 3 7	syl2anc	⊢ ( ω ≼ 𝐴 → ( ( 𝐴 × 𝐴 ) ⊔ 𝐴 ) ≈ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )
9		domentr	⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( ( 𝐴 × 𝐴 ) ⊔ 𝐴 ) ∧ ( ( 𝐴 × 𝐴 ) ⊔ 𝐴 ) ≈ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ) → ( 𝐴 × 𝐴 ) ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )
10	6 8 9	syl2anc	⊢ ( ω ≼ 𝐴 → ( 𝐴 × 𝐴 ) ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )
11		domtr	⊢ ( ( 𝒫 𝐴 ≼ ( 𝐴 × 𝐴 ) ∧ ( 𝐴 × 𝐴 ) ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ) → 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )
12	11	expcom	⊢ ( ( 𝐴 × 𝐴 ) ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) → ( 𝒫 𝐴 ≼ ( 𝐴 × 𝐴 ) → 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ) )
13	10 12	syl	⊢ ( ω ≼ 𝐴 → ( 𝒫 𝐴 ≼ ( 𝐴 × 𝐴 ) → 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ) )
14	1 13	mtod	⊢ ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ( 𝐴 × 𝐴 ) )