Metamath Proof Explorer

Theorem xpdom1g

Description: Dominance law for Cartesian product. Theorem 6L(c) of Enderton p. 149. (Contributed by NM, 25-Mar-2006) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion xpdom1g 
|- ( ( C e. V /\ A ~<_ B ) -> ( A X. C ) ~<_ ( B X. C ) )

Proof

Step Hyp Ref Expression
1 reldom 
 |-  Rel ~<_
2 1 brrelex1i 
 |-  ( A ~<_ B -> A e. _V )
3 xpcomeng 
 |-  ( ( A e. _V /\ C e. V ) -> ( A X. C ) ~~ ( C X. A ) )
4 3 ancoms 
 |-  ( ( C e. V /\ A e. _V ) -> ( A X. C ) ~~ ( C X. A ) )
5 2 4 sylan2 
 |-  ( ( C e. V /\ A ~<_ B ) -> ( A X. C ) ~~ ( C X. A ) )
6 xpdom2g 
 |-  ( ( C e. V /\ A ~<_ B ) -> ( C X. A ) ~<_ ( C X. B ) )
7 1 brrelex2i 
 |-  ( A ~<_ B -> B e. _V )
8 xpcomeng 
 |-  ( ( C e. V /\ B e. _V ) -> ( C X. B ) ~~ ( B X. C ) )
9 7 8 sylan2 
 |-  ( ( C e. V /\ A ~<_ B ) -> ( C X. B ) ~~ ( B X. C ) )
10 domentr 
 |-  ( ( ( C X. A ) ~<_ ( C X. B ) /\ ( C X. B ) ~~ ( B X. C ) ) -> ( C X. A ) ~<_ ( B X. C ) )
11 6 9 10 syl2anc 
 |-  ( ( C e. V /\ A ~<_ B ) -> ( C X. A ) ~<_ ( B X. C ) )
12 endomtr 
 |-  ( ( ( A X. C ) ~~ ( C X. A ) /\ ( C X. A ) ~<_ ( B X. C ) ) -> ( A X. C ) ~<_ ( B X. C ) )
13 5 11 12 syl2anc 
 |-  ( ( C e. V /\ A ~<_ B ) -> ( A X. C ) ~<_ ( B X. C ) )