Theorem undjudom

Description: Cardinal addition dominates union. (Contributed by NM, 28-Sep-2004) (Revised by Jim Kingdon, 15-Aug-2023)

	Ref	Expression
Assertion	undjudom	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\cup B\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		xpsnen2g	$$⊢\left(\varnothing \in \mathrm{V}\wedge A\in V\right)\to \left(\left\{\varnothing \right\}\times A\right)\approx A$$
3	1 2	mpan	$$⊢A\in V\to \left(\left\{\varnothing \right\}\times A\right)\approx A$$
4		ensym	$$⊢\left(\left\{\varnothing \right\}\times A\right)\approx A\to A\approx \left(\left\{\varnothing \right\}\times A\right)$$
5		endom	$$⊢A\approx \left(\left\{\varnothing \right\}\times A\right)\to A\preccurlyeq \left(\left\{\varnothing \right\}\times A\right)$$
6	3 4 5	3syl	$$⊢A\in V\to A\preccurlyeq \left(\left\{\varnothing \right\}\times A\right)$$
7		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
8		xpsnen2g	$$⊢\left(1_{𝑜}\in \mathrm{On}\wedge B\in W\right)\to \left(\left\{1_{𝑜}\right\}\times B\right)\approx B$$
9	7 8	mpan	$$⊢B\in W\to \left(\left\{1_{𝑜}\right\}\times B\right)\approx B$$
10		ensym	$$⊢\left(\left\{1_{𝑜}\right\}\times B\right)\approx B\to B\approx \left(\left\{1_{𝑜}\right\}\times B\right)$$
11		endom	$$⊢B\approx \left(\left\{1_{𝑜}\right\}\times B\right)\to B\preccurlyeq \left(\left\{1_{𝑜}\right\}\times B\right)$$
12	9 10 11	3syl	$$⊢B\in W\to B\preccurlyeq \left(\left\{1_{𝑜}\right\}\times B\right)$$
13		xp01disjl	$$⊢\left(\left\{\varnothing \right\}\times A\right)\cap \left(\left\{1_{𝑜}\right\}\times B\right)=\varnothing$$
14		undom	$$⊢\left(\left(A\preccurlyeq \left(\left\{\varnothing \right\}\times A\right)\wedge B\preccurlyeq \left(\left\{1_{𝑜}\right\}\times B\right)\right)\wedge \left(\left\{\varnothing \right\}\times A\right)\cap \left(\left\{1_{𝑜}\right\}\times B\right)=\varnothing \right)\to \left(A\cup B\right)\preccurlyeq \left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times B\right)\right)$$
15	13 14	mpan2	$$⊢\left(A\preccurlyeq \left(\left\{\varnothing \right\}\times A\right)\wedge B\preccurlyeq \left(\left\{1_{𝑜}\right\}\times B\right)\right)\to \left(A\cup B\right)\preccurlyeq \left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times B\right)\right)$$
16	6 12 15	syl2an	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\cup B\right)\preccurlyeq \left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times B\right)\right)$$
17		df-dju	$$⊢\left(A\mathrm{\bigsqcup ︀}B\right)=\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times B\right)$$
18	16 17	breqtrrdi	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\cup B\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)$$