Theorem pwdjudom

Description: A property of dominance over a powerset, and a main lemma for gchac . Similar to Lemma 2.3 of KanamoriPincus p. 420. (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	pwdjudom	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to 𝒫A\preccurlyeq B$$

Proof

Step	Hyp	Ref	Expression
1		canthwdom	$$⊢\neg 𝒫A{\preccurlyeq }^{*}A$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
4	3	brrelex2i	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\in \mathrm{V}$$
5		djuexb	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\leftrightarrow \left(A\mathrm{\bigsqcup ︀}B\right)\in \mathrm{V}$$
6	4 5	sylibr	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
7	6	simpld	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to A\in \mathrm{V}$$
8		xpsnen2g	$$⊢\left(\varnothing \in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \left(\left\{\varnothing \right\}\times A\right)\approx A$$
9	2 7 8	sylancr	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to \left(\left\{\varnothing \right\}\times A\right)\approx A$$
10		endom	$$⊢\left(\left\{\varnothing \right\}\times A\right)\approx A\to \left(\left\{\varnothing \right\}\times A\right)\preccurlyeq A$$
11		domwdom	$$⊢\left(\left\{\varnothing \right\}\times A\right)\preccurlyeq A\to \left(\left\{\varnothing \right\}\times A\right){\preccurlyeq }^{*}A$$
12		wdomtr	$$⊢\left(𝒫A{\preccurlyeq }^{*}\left(\left\{\varnothing \right\}\times A\right)\wedge \left(\left\{\varnothing \right\}\times A\right){\preccurlyeq }^{*}A\right)\to 𝒫A{\preccurlyeq }^{*}A$$
13	12	expcom	$$⊢\left(\left\{\varnothing \right\}\times A\right){\preccurlyeq }^{*}A\to \left(𝒫A{\preccurlyeq }^{*}\left(\left\{\varnothing \right\}\times A\right)\to 𝒫A{\preccurlyeq }^{*}A\right)$$
14	9 10 11 13	4syl	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to \left(𝒫A{\preccurlyeq }^{*}\left(\left\{\varnothing \right\}\times A\right)\to 𝒫A{\preccurlyeq }^{*}A\right)$$
15	1 14	mtoi	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to \neg 𝒫A{\preccurlyeq }^{*}\left(\left\{\varnothing \right\}\times A\right)$$
16		pwdjuen	$$⊢\left(A\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to 𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\approx \left(𝒫A\times 𝒫A\right)$$
17	7 7 16	syl2anc	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to 𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\approx \left(𝒫A\times 𝒫A\right)$$
18		domen1	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\approx \left(𝒫A\times 𝒫A\right)\to \left(𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\leftrightarrow \left(𝒫A\times 𝒫A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\right)$$
19	17 18	syl	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to \left(𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\leftrightarrow \left(𝒫A\times 𝒫A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\right)$$
20	19	ibi	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to \left(𝒫A\times 𝒫A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)$$
21		df-dju	$$⊢\left(A\mathrm{\bigsqcup ︀}B\right)=\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times B\right)$$
22	20 21	breqtrdi	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to \left(𝒫A\times 𝒫A\right)\preccurlyeq \left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times B\right)\right)$$
23		unxpwdom	$$⊢\left(𝒫A\times 𝒫A\right)\preccurlyeq \left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times B\right)\right)\to \left(𝒫A{\preccurlyeq }^{*}\left(\left\{\varnothing \right\}\times A\right)\vee 𝒫A\preccurlyeq \left(\left\{1_{𝑜}\right\}\times B\right)\right)$$
24	22 23	syl	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to \left(𝒫A{\preccurlyeq }^{*}\left(\left\{\varnothing \right\}\times A\right)\vee 𝒫A\preccurlyeq \left(\left\{1_{𝑜}\right\}\times B\right)\right)$$
25	24	ord	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to \left(\neg 𝒫A{\preccurlyeq }^{*}\left(\left\{\varnothing \right\}\times A\right)\to 𝒫A\preccurlyeq \left(\left\{1_{𝑜}\right\}\times B\right)\right)$$
26	15 25	mpd	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to 𝒫A\preccurlyeq \left(\left\{1_{𝑜}\right\}\times B\right)$$
27		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
28	6	simprd	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to B\in \mathrm{V}$$
29		xpsnen2g	$$⊢\left(1_{𝑜}\in \mathrm{On}\wedge B\in \mathrm{V}\right)\to \left(\left\{1_{𝑜}\right\}\times B\right)\approx B$$
30	27 28 29	sylancr	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to \left(\left\{1_{𝑜}\right\}\times B\right)\approx B$$
31		domentr	$$⊢\left(𝒫A\preccurlyeq \left(\left\{1_{𝑜}\right\}\times B\right)\wedge \left(\left\{1_{𝑜}\right\}\times B\right)\approx B\right)\to 𝒫A\preccurlyeq B$$
32	26 30 31	syl2anc	$$⊢𝒫\left(A\mathrm{\bigsqcup ︀}A\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\to 𝒫A\preccurlyeq B$$