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	$$⊢\mathrm{\omega }\preccurlyeq A\to \neg 𝒫A\preccurlyeq \left(A\times A\right)$$

Proof

Step	Hyp	Ref	Expression
1		pwxpndom2	$$⊢\mathrm{\omega }\preccurlyeq A\to \neg 𝒫A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}\left(A\times A\right)\right)$$
2		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
3	2	brrelex2i	$$⊢\mathrm{\omega }\preccurlyeq A\to A\in \mathrm{V}$$
4	3 3	xpexd	$$⊢\mathrm{\omega }\preccurlyeq A\to A\times A\in \mathrm{V}$$
5		djudoml	$$⊢\left(A\times A\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \left(A\times A\right)\preccurlyeq \left(\left(A\times A\right)\mathrm{\bigsqcup ︀}A\right)$$
6	4 3 5	syl2anc	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(A\times A\right)\preccurlyeq \left(\left(A\times A\right)\mathrm{\bigsqcup ︀}A\right)$$
7		djucomen	$$⊢\left(A\times A\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \left(\left(A\times A\right)\mathrm{\bigsqcup ︀}A\right)\approx \left(A\mathrm{\bigsqcup ︀}\left(A\times A\right)\right)$$
8	4 3 7	syl2anc	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(\left(A\times A\right)\mathrm{\bigsqcup ︀}A\right)\approx \left(A\mathrm{\bigsqcup ︀}\left(A\times A\right)\right)$$
9		domentr	$$⊢\left(\left(A\times A\right)\preccurlyeq \left(\left(A\times A\right)\mathrm{\bigsqcup ︀}A\right)\wedge \left(\left(A\times A\right)\mathrm{\bigsqcup ︀}A\right)\approx \left(A\mathrm{\bigsqcup ︀}\left(A\times A\right)\right)\right)\to \left(A\times A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}\left(A\times A\right)\right)$$
10	6 8 9	syl2anc	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(A\times A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}\left(A\times A\right)\right)$$
11		domtr	$$⊢\left(𝒫A\preccurlyeq \left(A\times A\right)\wedge \left(A\times A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}\left(A\times A\right)\right)\right)\to 𝒫A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}\left(A\times A\right)\right)$$
12	11	expcom	$$⊢\left(A\times A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}\left(A\times A\right)\right)\to \left(𝒫A\preccurlyeq \left(A\times A\right)\to 𝒫A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}\left(A\times A\right)\right)\right)$$
13	10 12	syl	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(𝒫A\preccurlyeq \left(A\times A\right)\to 𝒫A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}\left(A\times A\right)\right)\right)$$
14	1 13	mtod	$$⊢\mathrm{\omega }\preccurlyeq A\to \neg 𝒫A\preccurlyeq \left(A\times A\right)$$