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	$⊢ ω ≼ A \to \neg 𝒫 A ≼ (A \times A)$

Proof

Step	Hyp	Ref	Expression
1		pwxpndom2	$⊢ ω ≼ A \to \neg 𝒫 A ≼ (A ⊔︀ (A \times A))$
2		reldom	$⊢ Rel ≼$
3	2	brrelex2i	$⊢ ω ≼ A \to A \in V$
4	3 3	xpexd	$⊢ ω ≼ A \to A \times A \in V$
5		djudoml	$⊢ (A \times A \in V \land A \in V) \to (A \times A) ≼ ((A \times A) ⊔︀ A)$
6	4 3 5	syl2anc	$⊢ ω ≼ A \to (A \times A) ≼ ((A \times A) ⊔︀ A)$
7		djucomen	$⊢ (A \times A \in V \land A \in V) \to ((A \times A) ⊔︀ A) \approx (A ⊔︀ (A \times A))$
8	4 3 7	syl2anc	$⊢ ω ≼ A \to ((A \times A) ⊔︀ A) \approx (A ⊔︀ (A \times A))$
9		domentr	$⊢ ((A \times A) ≼ ((A \times A) ⊔︀ A) \land ((A \times A) ⊔︀ A) \approx (A ⊔︀ (A \times A))) \to (A \times A) ≼ (A ⊔︀ (A \times A))$
10	6 8 9	syl2anc	$⊢ ω ≼ A \to (A \times A) ≼ (A ⊔︀ (A \times A))$
11		domtr	$⊢ (𝒫 A ≼ (A \times A) \land (A \times A) ≼ (A ⊔︀ (A \times A))) \to 𝒫 A ≼ (A ⊔︀ (A \times A))$
12	11	expcom	$⊢ (A \times A) ≼ (A ⊔︀ (A \times A)) \to (𝒫 A ≼ (A \times A) \to 𝒫 A ≼ (A ⊔︀ (A \times A)))$
13	10 12	syl	$⊢ ω ≼ A \to (𝒫 A ≼ (A \times A) \to 𝒫 A ≼ (A ⊔︀ (A \times A)))$
14	1 13	mtod	$⊢ ω ≼ A \to \neg 𝒫 A ≼ (A \times A)$