# Metamath Proof Explorer

## 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}×{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}↔{1}_{𝑜}\prec {A}\right)$
6 5 anbi1d ${⊢}{x}={A}\to \left(\left({1}_{𝑜}\prec {x}\wedge {1}_{𝑜}\prec {y}\right)↔\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}×{y}={A}×{y}$
9 7 8 breq12d ${⊢}{x}={A}\to \left(\left({x}\cup {y}\right)\preccurlyeq \left({x}×{y}\right)↔\left({A}\cup {y}\right)\preccurlyeq \left({A}×{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}×{y}\right)\right)↔\left(\left({1}_{𝑜}\prec {A}\wedge {1}_{𝑜}\prec {y}\right)\to \left({A}\cup {y}\right)\preccurlyeq \left({A}×{y}\right)\right)\right)$
11 breq2 ${⊢}{y}={B}\to \left({1}_{𝑜}\prec {y}↔{1}_{𝑜}\prec {B}\right)$
12 11 anbi2d ${⊢}{y}={B}\to \left(\left({1}_{𝑜}\prec {A}\wedge {1}_{𝑜}\prec {y}\right)↔\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}×{y}={A}×{B}$
15 13 14 breq12d ${⊢}{y}={B}\to \left(\left({A}\cup {y}\right)\preccurlyeq \left({A}×{y}\right)↔\left({A}\cup {B}\right)\preccurlyeq \left({A}×{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}×{y}\right)\right)↔\left(\left({1}_{𝑜}\prec {A}\wedge {1}_{𝑜}\prec {B}\right)\to \left({A}\cup {B}\right)\preccurlyeq \left({A}×{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}×{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}×{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}×{B}\right)$