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	$$⊢\mathrm{\omega }\preccurlyeq A\to \neg 𝒫A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}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		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
3	2	xpeq1i	$$⊢1_{𝑜}\times A=\left\{\varnothing \right\}\times A$$
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
6	5	brrelex2i	$$⊢\mathrm{\omega }\preccurlyeq A\to A\in \mathrm{V}$$
7		xpsnen2g	$$⊢\left(\varnothing \in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \left(\left\{\varnothing \right\}\times A\right)\approx A$$
8	4 6 7	sylancr	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(\left\{\varnothing \right\}\times A\right)\approx A$$
9	3 8	eqbrtrid	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(1_{𝑜}\times A\right)\approx A$$
10	9	ensymd	$$⊢\mathrm{\omega }\preccurlyeq A\to A\approx \left(1_{𝑜}\times A\right)$$
11		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
12		ordom	$$⊢\mathrm{Ord}\mathrm{\omega }$$
13		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
14		ordelss	$$⊢\left(\mathrm{Ord}\mathrm{\omega }\wedge 1_{𝑜}\in \mathrm{\omega }\right)\to 1_{𝑜}\subseteq \mathrm{\omega }$$
15	12 13 14	mp2an	$$⊢1_{𝑜}\subseteq \mathrm{\omega }$$
16		ssdomg	$$⊢\mathrm{\omega }\in \mathrm{V}\to \left(1_{𝑜}\subseteq \mathrm{\omega }\to 1_{𝑜}\preccurlyeq \mathrm{\omega }\right)$$
17	11 15 16	mp2	$$⊢1_{𝑜}\preccurlyeq \mathrm{\omega }$$
18		domtr	$$⊢\left(1_{𝑜}\preccurlyeq \mathrm{\omega }\wedge \mathrm{\omega }\preccurlyeq A\right)\to 1_{𝑜}\preccurlyeq A$$
19	17 18	mpan	$$⊢\mathrm{\omega }\preccurlyeq A\to 1_{𝑜}\preccurlyeq A$$
20		xpdom1g	$$⊢\left(A\in \mathrm{V}\wedge 1_{𝑜}\preccurlyeq A\right)\to \left(1_{𝑜}\times A\right)\preccurlyeq \left(A\times A\right)$$
21	6 19 20	syl2anc	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(1_{𝑜}\times A\right)\preccurlyeq \left(A\times A\right)$$
22		endomtr	$$⊢\left(A\approx \left(1_{𝑜}\times A\right)\wedge \left(1_{𝑜}\times A\right)\preccurlyeq \left(A\times A\right)\right)\to A\preccurlyeq \left(A\times A\right)$$
23	10 21 22	syl2anc	$$⊢\mathrm{\omega }\preccurlyeq A\to A\preccurlyeq \left(A\times A\right)$$
24		djudom2	$$⊢\left(A\preccurlyeq \left(A\times A\right)\wedge A\in \mathrm{V}\right)\to \left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}\left(A\times A\right)\right)$$
25	23 6 24	syl2anc	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}\left(A\times A\right)\right)$$
26		domtr	$$⊢\left(𝒫A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}A\right)\wedge \left(A\mathrm{\bigsqcup ︀}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)$$
27	26	expcom	$$⊢\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}\left(A\times A\right)\right)\to \left(𝒫A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}A\right)\to 𝒫A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}\left(A\times A\right)\right)\right)$$
28	25 27	syl	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(𝒫A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}A\right)\to 𝒫A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}\left(A\times A\right)\right)\right)$$
29	1 28	mtod	$$⊢\mathrm{\omega }\preccurlyeq A\to \neg 𝒫A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}A\right)$$