Metamath Proof Explorer

Theorem djudom1

Description: Ordering law for cardinal addition. Exercise 4.56(f) of Mendelson p. 258. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015) (Revised by Jim Kingdon, 1-Sep-2023)

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

Proof

Step Hyp Ref Expression
1 snex 
 |-  { (/) } e. _V
2 1 xpdom2 
 |-  ( A ~<_ B -> ( { (/) } X. A ) ~<_ ( { (/) } X. B ) )
3 snex 
 |-  { 1o } e. _V
4 xpexg 
 |-  ( ( { 1o } e. _V /\ C e. V ) -> ( { 1o } X. C ) e. _V )
5 3 4 mpan 
 |-  ( C e. V -> ( { 1o } X. C ) e. _V )
6 domrefg 
 |-  ( ( { 1o } X. C ) e. _V -> ( { 1o } X. C ) ~<_ ( { 1o } X. C ) )
7 5 6 syl 
 |-  ( C e. V -> ( { 1o } X. C ) ~<_ ( { 1o } X. C ) )
8 xp01disjl 
 |-  ( ( { (/) } X. B ) i^i ( { 1o } X. C ) ) = (/)
9 undom 
 |-  ( ( ( ( { (/) } X. A ) ~<_ ( { (/) } X. B ) /\ ( { 1o } X. C ) ~<_ ( { 1o } X. C ) ) /\ ( ( { (/) } X. B ) i^i ( { 1o } X. C ) ) = (/) ) -> ( ( { (/) } X. A ) u. ( { 1o } X. C ) ) ~<_ ( ( { (/) } X. B ) u. ( { 1o } X. C ) ) )
10 8 9 mpan2 
 |-  ( ( ( { (/) } X. A ) ~<_ ( { (/) } X. B ) /\ ( { 1o } X. C ) ~<_ ( { 1o } X. C ) ) -> ( ( { (/) } X. A ) u. ( { 1o } X. C ) ) ~<_ ( ( { (/) } X. B ) u. ( { 1o } X. C ) ) )
11 2 7 10 syl2an 
 |-  ( ( A ~<_ B /\ C e. V ) -> ( ( { (/) } X. A ) u. ( { 1o } X. C ) ) ~<_ ( ( { (/) } X. B ) u. ( { 1o } X. C ) ) )
12 df-dju 
 |-  ( A |_| C ) = ( ( { (/) } X. A ) u. ( { 1o } X. C ) )
13 df-dju 
 |-  ( B |_| C ) = ( ( { (/) } X. B ) u. ( { 1o } X. C ) )
14 11 12 13 3brtr4g 
 |-  ( ( A ~<_ B /\ C e. V ) -> ( A |_| C ) ~<_ ( B |_| C ) )