Theorem xpen

Description: Equinumerosity law for Cartesian product. Proposition 4.22(b) of Mendelson p. 254. (Contributed by NM, 24-Jul-2004) (Proof shortened by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	xpen	$$⊢\left(A\approx B\wedge C\approx D\right)\to \left(A\times C\right)\approx \left(B\times D\right)$$

Proof

Step	Hyp	Ref	Expression
1		relen	$$⊢\mathrm{Rel}\approx$$
2	1	brrelex1i	$$⊢C\approx D\to C\in \mathrm{V}$$
3		endom	$$⊢A\approx B\to A\preccurlyeq B$$
4		xpdom1g	$$⊢\left(C\in \mathrm{V}\wedge A\preccurlyeq B\right)\to \left(A\times C\right)\preccurlyeq \left(B\times C\right)$$
5	2 3 4	syl2anr	$$⊢\left(A\approx B\wedge C\approx D\right)\to \left(A\times C\right)\preccurlyeq \left(B\times C\right)$$
6	1	brrelex2i	$$⊢A\approx B\to B\in \mathrm{V}$$
7		endom	$$⊢C\approx D\to C\preccurlyeq D$$
8		xpdom2g	$$⊢\left(B\in \mathrm{V}\wedge C\preccurlyeq D\right)\to \left(B\times C\right)\preccurlyeq \left(B\times D\right)$$
9	6 7 8	syl2an	$$⊢\left(A\approx B\wedge C\approx D\right)\to \left(B\times C\right)\preccurlyeq \left(B\times D\right)$$
10		domtr	$$⊢\left(\left(A\times C\right)\preccurlyeq \left(B\times C\right)\wedge \left(B\times C\right)\preccurlyeq \left(B\times D\right)\right)\to \left(A\times C\right)\preccurlyeq \left(B\times D\right)$$
11	5 9 10	syl2anc	$$⊢\left(A\approx B\wedge C\approx D\right)\to \left(A\times C\right)\preccurlyeq \left(B\times D\right)$$
12	1	brrelex2i	$$⊢C\approx D\to D\in \mathrm{V}$$
13		ensym	$$⊢A\approx B\to B\approx A$$
14		endom	$$⊢B\approx A\to B\preccurlyeq A$$
15	13 14	syl	$$⊢A\approx B\to B\preccurlyeq A$$
16		xpdom1g	$$⊢\left(D\in \mathrm{V}\wedge B\preccurlyeq A\right)\to \left(B\times D\right)\preccurlyeq \left(A\times D\right)$$
17	12 15 16	syl2anr	$$⊢\left(A\approx B\wedge C\approx D\right)\to \left(B\times D\right)\preccurlyeq \left(A\times D\right)$$
18	1	brrelex1i	$$⊢A\approx B\to A\in \mathrm{V}$$
19		ensym	$$⊢C\approx D\to D\approx C$$
20		endom	$$⊢D\approx C\to D\preccurlyeq C$$
21	19 20	syl	$$⊢C\approx D\to D\preccurlyeq C$$
22		xpdom2g	$$⊢\left(A\in \mathrm{V}\wedge D\preccurlyeq C\right)\to \left(A\times D\right)\preccurlyeq \left(A\times C\right)$$
23	18 21 22	syl2an	$$⊢\left(A\approx B\wedge C\approx D\right)\to \left(A\times D\right)\preccurlyeq \left(A\times C\right)$$
24		domtr	$$⊢\left(\left(B\times D\right)\preccurlyeq \left(A\times D\right)\wedge \left(A\times D\right)\preccurlyeq \left(A\times C\right)\right)\to \left(B\times D\right)\preccurlyeq \left(A\times C\right)$$
25	17 23 24	syl2anc	$$⊢\left(A\approx B\wedge C\approx D\right)\to \left(B\times D\right)\preccurlyeq \left(A\times C\right)$$
26		sbth	$$⊢\left(\left(A\times C\right)\preccurlyeq \left(B\times D\right)\wedge \left(B\times D\right)\preccurlyeq \left(A\times C\right)\right)\to \left(A\times C\right)\approx \left(B\times D\right)$$
27	11 25 26	syl2anc	$$⊢\left(A\approx B\wedge C\approx D\right)\to \left(A\times C\right)\approx \left(B\times D\right)$$