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

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

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