Theorem djuxpdom

Description: Cartesian product dominates disjoint union for sets with cardinality greater than 1. Similar to Proposition 10.36 of TakeutiZaring p. 93. (Contributed by Mario Carneiro, 18-May-2015)

	Ref	Expression
Assertion	djuxpdom	$$⊢\left(1_{𝑜}\prec A\wedge 1_{𝑜}\prec B\right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\preccurlyeq \left(A\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-dju	$$⊢\left(A\mathrm{\bigsqcup ︀}B\right)=\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times B\right)$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3		relsdom	$$⊢\mathrm{Rel}\prec$$
4	3	brrelex2i	$$⊢1_{𝑜}\prec A\to A\in \mathrm{V}$$
5		xpsnen2g	$$⊢\left(\varnothing \in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \left(\left\{\varnothing \right\}\times A\right)\approx A$$
6	2 4 5	sylancr	$$⊢1_{𝑜}\prec A\to \left(\left\{\varnothing \right\}\times A\right)\approx A$$
7		sdomen2	$$⊢\left(\left\{\varnothing \right\}\times A\right)\approx A\to \left(1_{𝑜}\prec \left(\left\{\varnothing \right\}\times A\right)\leftrightarrow 1_{𝑜}\prec A\right)$$
8	6 7	syl	$$⊢1_{𝑜}\prec A\to \left(1_{𝑜}\prec \left(\left\{\varnothing \right\}\times A\right)\leftrightarrow 1_{𝑜}\prec A\right)$$
9	8	ibir	$$⊢1_{𝑜}\prec A\to 1_{𝑜}\prec \left(\left\{\varnothing \right\}\times A\right)$$
10		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
11	3	brrelex2i	$$⊢1_{𝑜}\prec B\to B\in \mathrm{V}$$
12		xpsnen2g	$$⊢\left(1_{𝑜}\in \mathrm{On}\wedge B\in \mathrm{V}\right)\to \left(\left\{1_{𝑜}\right\}\times B\right)\approx B$$
13	10 11 12	sylancr	$$⊢1_{𝑜}\prec B\to \left(\left\{1_{𝑜}\right\}\times B\right)\approx B$$
14		sdomen2	$$⊢\left(\left\{1_{𝑜}\right\}\times B\right)\approx B\to \left(1_{𝑜}\prec \left(\left\{1_{𝑜}\right\}\times B\right)\leftrightarrow 1_{𝑜}\prec B\right)$$
15	13 14	syl	$$⊢1_{𝑜}\prec B\to \left(1_{𝑜}\prec \left(\left\{1_{𝑜}\right\}\times B\right)\leftrightarrow 1_{𝑜}\prec B\right)$$
16	15	ibir	$$⊢1_{𝑜}\prec B\to 1_{𝑜}\prec \left(\left\{1_{𝑜}\right\}\times B\right)$$
17		unxpdom	$$⊢\left(1_{𝑜}\prec \left(\left\{\varnothing \right\}\times A\right)\wedge 1_{𝑜}\prec \left(\left\{1_{𝑜}\right\}\times B\right)\right)\to \left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times B\right)\right)\preccurlyeq \left(\left(\left\{\varnothing \right\}\times A\right)\times \left(\left\{1_{𝑜}\right\}\times B\right)\right)$$
18	9 16 17	syl2an	$$⊢\left(1_{𝑜}\prec A\wedge 1_{𝑜}\prec B\right)\to \left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times B\right)\right)\preccurlyeq \left(\left(\left\{\varnothing \right\}\times A\right)\times \left(\left\{1_{𝑜}\right\}\times B\right)\right)$$
19	1 18	eqbrtrid	$$⊢\left(1_{𝑜}\prec A\wedge 1_{𝑜}\prec B\right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\preccurlyeq \left(\left(\left\{\varnothing \right\}\times A\right)\times \left(\left\{1_{𝑜}\right\}\times B\right)\right)$$
20		xpen	$$⊢\left(\left(\left\{\varnothing \right\}\times A\right)\approx A\wedge \left(\left\{1_{𝑜}\right\}\times B\right)\approx B\right)\to \left(\left(\left\{\varnothing \right\}\times A\right)\times \left(\left\{1_{𝑜}\right\}\times B\right)\right)\approx \left(A\times B\right)$$
21	6 13 20	syl2an	$$⊢\left(1_{𝑜}\prec A\wedge 1_{𝑜}\prec B\right)\to \left(\left(\left\{\varnothing \right\}\times A\right)\times \left(\left\{1_{𝑜}\right\}\times B\right)\right)\approx \left(A\times B\right)$$
22		domentr	$$⊢\left(\left(A\mathrm{\bigsqcup ︀}B\right)\preccurlyeq \left(\left(\left\{\varnothing \right\}\times A\right)\times \left(\left\{1_{𝑜}\right\}\times B\right)\right)\wedge \left(\left(\left\{\varnothing \right\}\times A\right)\times \left(\left\{1_{𝑜}\right\}\times B\right)\right)\approx \left(A\times B\right)\right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\preccurlyeq \left(A\times B\right)$$
23	19 21 22	syl2anc	$$⊢\left(1_{𝑜}\prec A\wedge 1_{𝑜}\prec B\right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\preccurlyeq \left(A\times B\right)$$