Theorem unxpdom

Description: Cartesian product dominates union for sets with cardinality greater than 1. Proposition 10.36 of TakeutiZaring p. 93. (Contributed by Mario Carneiro, 13-Jan-2013) (Proof shortened by Mario Carneiro, 27-Apr-2015)

	Ref	Expression
Assertion	unxpdom	$$⊢\left(1_{𝑜}\prec A\wedge 1_{𝑜}\prec B\right)\to \left(A\cup B\right)\preccurlyeq \left(A\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		relsdom	$$⊢\mathrm{Rel}\prec$$
2	1	brrelex2i	$$⊢1_{𝑜}\prec A\to A\in \mathrm{V}$$
3	1	brrelex2i	$$⊢1_{𝑜}\prec B\to B\in \mathrm{V}$$
4	2 3	anim12i	$$⊢\left(1_{𝑜}\prec A\wedge 1_{𝑜}\prec B\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
5		breq2	$$⊢x=A\to \left(1_{𝑜}\prec x\leftrightarrow 1_{𝑜}\prec A\right)$$
6	5	anbi1d	$$⊢x=A\to \left(\left(1_{𝑜}\prec x\wedge 1_{𝑜}\prec y\right)\leftrightarrow \left(1_{𝑜}\prec A\wedge 1_{𝑜}\prec y\right)\right)$$
7		uneq1	$$⊢x=A\to x\cup y=A\cup y$$
8		xpeq1	$$⊢x=A\to x\times y=A\times y$$
9	7 8	breq12d	$$⊢x=A\to \left(\left(x\cup y\right)\preccurlyeq \left(x\times y\right)\leftrightarrow \left(A\cup y\right)\preccurlyeq \left(A\times y\right)\right)$$
10	6 9	imbi12d	$$⊢x=A\to \left(\left(\left(1_{𝑜}\prec x\wedge 1_{𝑜}\prec y\right)\to \left(x\cup y\right)\preccurlyeq \left(x\times y\right)\right)\leftrightarrow \left(\left(1_{𝑜}\prec A\wedge 1_{𝑜}\prec y\right)\to \left(A\cup y\right)\preccurlyeq \left(A\times y\right)\right)\right)$$
11		breq2	$$⊢y=B\to \left(1_{𝑜}\prec y\leftrightarrow 1_{𝑜}\prec B\right)$$
12	11	anbi2d	$$⊢y=B\to \left(\left(1_{𝑜}\prec A\wedge 1_{𝑜}\prec y\right)\leftrightarrow \left(1_{𝑜}\prec A\wedge 1_{𝑜}\prec B\right)\right)$$
13		uneq2	$$⊢y=B\to A\cup y=A\cup B$$
14		xpeq2	$$⊢y=B\to A\times y=A\times B$$
15	13 14	breq12d	$$⊢y=B\to \left(\left(A\cup y\right)\preccurlyeq \left(A\times y\right)\leftrightarrow \left(A\cup B\right)\preccurlyeq \left(A\times B\right)\right)$$
16	12 15	imbi12d	$$⊢y=B\to \left(\left(\left(1_{𝑜}\prec A\wedge 1_{𝑜}\prec y\right)\to \left(A\cup y\right)\preccurlyeq \left(A\times y\right)\right)\leftrightarrow \left(\left(1_{𝑜}\prec A\wedge 1_{𝑜}\prec B\right)\to \left(A\cup B\right)\preccurlyeq \left(A\times B\right)\right)\right)$$
17		eqid	$$⊢\left(z\in \left(x\cup y\right)⟼if\left(z\in x,⟨z,if\left(z=v,w,t\right)⟩,⟨if\left(z=w,u,v\right),z⟩\right)\right)=\left(z\in \left(x\cup y\right)⟼if\left(z\in x,⟨z,if\left(z=v,w,t\right)⟩,⟨if\left(z=w,u,v\right),z⟩\right)\right)$$
18		eqid	$$⊢if\left(z\in x,⟨z,if\left(z=v,w,t\right)⟩,⟨if\left(z=w,u,v\right),z⟩\right)=if\left(z\in x,⟨z,if\left(z=v,w,t\right)⟩,⟨if\left(z=w,u,v\right),z⟩\right)$$
19	17 18	unxpdomlem3	$$⊢\left(1_{𝑜}\prec x\wedge 1_{𝑜}\prec y\right)\to \left(x\cup y\right)\preccurlyeq \left(x\times y\right)$$
20	10 16 19	vtocl2g	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(\left(1_{𝑜}\prec A\wedge 1_{𝑜}\prec B\right)\to \left(A\cup B\right)\preccurlyeq \left(A\times B\right)\right)$$
21	4 20	mpcom	$$⊢\left(1_{𝑜}\prec A\wedge 1_{𝑜}\prec B\right)\to \left(A\cup B\right)\preccurlyeq \left(A\times B\right)$$