Metamath Proof Explorer

Theorem djudom2

Description: Ordering law for cardinal addition. Theorem 6L(a) of Enderton p. 149. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 djudom1 
 |-  ( ( A ~<_ B /\ C e. V ) -> ( A |_| C ) ~<_ ( B |_| C ) )
2 reldom 
 |-  Rel ~<_
3 2 brrelex1i 
 |-  ( A ~<_ B -> A e. _V )
4 djucomen 
 |-  ( ( A e. _V /\ C e. V ) -> ( A |_| C ) ~~ ( C |_| A ) )
5 3 4 sylan 
 |-  ( ( A ~<_ B /\ C e. V ) -> ( A |_| C ) ~~ ( C |_| A ) )
6 2 brrelex2i 
 |-  ( A ~<_ B -> B e. _V )
7 djucomen 
 |-  ( ( B e. _V /\ C e. V ) -> ( B |_| C ) ~~ ( C |_| B ) )
8 6 7 sylan 
 |-  ( ( A ~<_ B /\ C e. V ) -> ( B |_| C ) ~~ ( C |_| B ) )
9 domen1 
 |-  ( ( A |_| C ) ~~ ( C |_| A ) -> ( ( A |_| C ) ~<_ ( B |_| C ) <-> ( C |_| A ) ~<_ ( B |_| C ) ) )
10 domen2 
 |-  ( ( B |_| C ) ~~ ( C |_| B ) -> ( ( C |_| A ) ~<_ ( B |_| C ) <-> ( C |_| A ) ~<_ ( C |_| B ) ) )
11 9 10 sylan9bb 
 |-  ( ( ( A |_| C ) ~~ ( C |_| A ) /\ ( B |_| C ) ~~ ( C |_| B ) ) -> ( ( A |_| C ) ~<_ ( B |_| C ) <-> ( C |_| A ) ~<_ ( C |_| B ) ) )
12 5 8 11 syl2anc 
 |-  ( ( A ~<_ B /\ C e. V ) -> ( ( A |_| C ) ~<_ ( B |_| C ) <-> ( C |_| A ) ~<_ ( C |_| B ) ) )
13 1 12 mpbid 
 |-  ( ( A ~<_ B /\ C e. V ) -> ( C |_| A ) ~<_ ( C |_| B ) )