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 
|- ( ( A ~~ B /\ C ~~ D ) -> ( A X. C ) ~~ ( B X. D ) )

Proof

Step Hyp Ref Expression
1 relen 
 |-  Rel ~~
2 1 brrelex1i 
 |-  ( C ~~ D -> C e. _V )
3 endom 
 |-  ( A ~~ B -> A ~<_ B )
4 xpdom1g 
 |-  ( ( C e. _V /\ A ~<_ B ) -> ( A X. C ) ~<_ ( B X. C ) )
5 2 3 4 syl2anr 
 |-  ( ( A ~~ B /\ C ~~ D ) -> ( A X. C ) ~<_ ( B X. C ) )
6 1 brrelex2i 
 |-  ( A ~~ B -> B e. _V )
7 endom 
 |-  ( C ~~ D -> C ~<_ D )
8 xpdom2g 
 |-  ( ( B e. _V /\ C ~<_ D ) -> ( B X. C ) ~<_ ( B X. D ) )
9 6 7 8 syl2an 
 |-  ( ( A ~~ B /\ C ~~ D ) -> ( B X. C ) ~<_ ( B X. D ) )
10 domtr 
 |-  ( ( ( A X. C ) ~<_ ( B X. C ) /\ ( B X. C ) ~<_ ( B X. D ) ) -> ( A X. C ) ~<_ ( B X. D ) )
11 5 9 10 syl2anc 
 |-  ( ( A ~~ B /\ C ~~ D ) -> ( A X. C ) ~<_ ( B X. D ) )
12 1 brrelex2i 
 |-  ( C ~~ D -> D e. _V )
13 ensym 
 |-  ( A ~~ B -> B ~~ A )
14 endom 
 |-  ( B ~~ A -> B ~<_ A )
15 13 14 syl 
 |-  ( A ~~ B -> B ~<_ A )
16 xpdom1g 
 |-  ( ( D e. _V /\ B ~<_ A ) -> ( B X. D ) ~<_ ( A X. D ) )
17 12 15 16 syl2anr 
 |-  ( ( A ~~ B /\ C ~~ D ) -> ( B X. D ) ~<_ ( A X. D ) )
18 1 brrelex1i 
 |-  ( A ~~ B -> A e. _V )
19 ensym 
 |-  ( C ~~ D -> D ~~ C )
20 endom 
 |-  ( D ~~ C -> D ~<_ C )
21 19 20 syl 
 |-  ( C ~~ D -> D ~<_ C )
22 xpdom2g 
 |-  ( ( A e. _V /\ D ~<_ C ) -> ( A X. D ) ~<_ ( A X. C ) )
23 18 21 22 syl2an 
 |-  ( ( A ~~ B /\ C ~~ D ) -> ( A X. D ) ~<_ ( A X. C ) )
24 domtr 
 |-  ( ( ( B X. D ) ~<_ ( A X. D ) /\ ( A X. D ) ~<_ ( A X. C ) ) -> ( B X. D ) ~<_ ( A X. C ) )
25 17 23 24 syl2anc 
 |-  ( ( A ~~ B /\ C ~~ D ) -> ( B X. D ) ~<_ ( A X. C ) )
26 sbth 
 |-  ( ( ( A X. C ) ~<_ ( B X. D ) /\ ( B X. D ) ~<_ ( A X. C ) ) -> ( A X. C ) ~~ ( B X. D ) )
27 11 25 26 syl2anc 
 |-  ( ( A ~~ B /\ C ~~ D ) -> ( A X. C ) ~~ ( B X. D ) )