Metamath Proof Explorer

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}×{C}\right)\approx \left({B}×{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}×{C}\right)\preccurlyeq \left({B}×{C}\right)$
5 2 3 4 syl2anr ${⊢}\left({A}\approx {B}\wedge {C}\approx {D}\right)\to \left({A}×{C}\right)\preccurlyeq \left({B}×{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}×{C}\right)\preccurlyeq \left({B}×{D}\right)$
9 6 7 8 syl2an ${⊢}\left({A}\approx {B}\wedge {C}\approx {D}\right)\to \left({B}×{C}\right)\preccurlyeq \left({B}×{D}\right)$
10 domtr ${⊢}\left(\left({A}×{C}\right)\preccurlyeq \left({B}×{C}\right)\wedge \left({B}×{C}\right)\preccurlyeq \left({B}×{D}\right)\right)\to \left({A}×{C}\right)\preccurlyeq \left({B}×{D}\right)$
11 5 9 10 syl2anc ${⊢}\left({A}\approx {B}\wedge {C}\approx {D}\right)\to \left({A}×{C}\right)\preccurlyeq \left({B}×{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}×{D}\right)\preccurlyeq \left({A}×{D}\right)$
17 12 15 16 syl2anr ${⊢}\left({A}\approx {B}\wedge {C}\approx {D}\right)\to \left({B}×{D}\right)\preccurlyeq \left({A}×{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}×{D}\right)\preccurlyeq \left({A}×{C}\right)$
23 18 21 22 syl2an ${⊢}\left({A}\approx {B}\wedge {C}\approx {D}\right)\to \left({A}×{D}\right)\preccurlyeq \left({A}×{C}\right)$
24 domtr ${⊢}\left(\left({B}×{D}\right)\preccurlyeq \left({A}×{D}\right)\wedge \left({A}×{D}\right)\preccurlyeq \left({A}×{C}\right)\right)\to \left({B}×{D}\right)\preccurlyeq \left({A}×{C}\right)$
25 17 23 24 syl2anc ${⊢}\left({A}\approx {B}\wedge {C}\approx {D}\right)\to \left({B}×{D}\right)\preccurlyeq \left({A}×{C}\right)$
26 sbth ${⊢}\left(\left({A}×{C}\right)\preccurlyeq \left({B}×{D}\right)\wedge \left({B}×{D}\right)\preccurlyeq \left({A}×{C}\right)\right)\to \left({A}×{C}\right)\approx \left({B}×{D}\right)$
27 11 25 26 syl2anc ${⊢}\left({A}\approx {B}\wedge {C}\approx {D}\right)\to \left({A}×{C}\right)\approx \left({B}×{D}\right)$