Metamath Proof Explorer

Theorem djuxpdom

Description: Cartesian product dominates disjoint union for sets with cardinality greater than 1. Similar to Proposition 10.36 of TakeutiZaring p. 93. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion djuxpdom 
|- ( ( 1o ~< A /\ 1o ~< B ) -> ( A |_| B ) ~<_ ( A X. B ) )

Proof

Step Hyp Ref Expression
1 df-dju 
 |-  ( A |_| B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
2 0ex 
 |-  (/) e. _V
3 relsdom 
 |-  Rel ~<
4 3 brrelex2i 
 |-  ( 1o ~< A -> A e. _V )
5 xpsnen2g 
 |-  ( ( (/) e. _V /\ A e. _V ) -> ( { (/) } X. A ) ~~ A )
6 2 4 5 sylancr 
 |-  ( 1o ~< A -> ( { (/) } X. A ) ~~ A )
7 sdomen2 
 |-  ( ( { (/) } X. A ) ~~ A -> ( 1o ~< ( { (/) } X. A ) <-> 1o ~< A ) )
8 6 7 syl 
 |-  ( 1o ~< A -> ( 1o ~< ( { (/) } X. A ) <-> 1o ~< A ) )
9 8 ibir 
 |-  ( 1o ~< A -> 1o ~< ( { (/) } X. A ) )
10 1on 
 |-  1o e. On
11 3 brrelex2i 
 |-  ( 1o ~< B -> B e. _V )
12 xpsnen2g 
 |-  ( ( 1o e. On /\ B e. _V ) -> ( { 1o } X. B ) ~~ B )
13 10 11 12 sylancr 
 |-  ( 1o ~< B -> ( { 1o } X. B ) ~~ B )
14 sdomen2 
 |-  ( ( { 1o } X. B ) ~~ B -> ( 1o ~< ( { 1o } X. B ) <-> 1o ~< B ) )
15 13 14 syl 
 |-  ( 1o ~< B -> ( 1o ~< ( { 1o } X. B ) <-> 1o ~< B ) )
16 15 ibir 
 |-  ( 1o ~< B -> 1o ~< ( { 1o } X. B ) )
17 unxpdom 
 |-  ( ( 1o ~< ( { (/) } X. A ) /\ 1o ~< ( { 1o } X. B ) ) -> ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) ~<_ ( ( { (/) } X. A ) X. ( { 1o } X. B ) ) )
18 9 16 17 syl2an 
 |-  ( ( 1o ~< A /\ 1o ~< B ) -> ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) ~<_ ( ( { (/) } X. A ) X. ( { 1o } X. B ) ) )
19 1 18 eqbrtrid 
 |-  ( ( 1o ~< A /\ 1o ~< B ) -> ( A |_| B ) ~<_ ( ( { (/) } X. A ) X. ( { 1o } X. B ) ) )
20 xpen 
 |-  ( ( ( { (/) } X. A ) ~~ A /\ ( { 1o } X. B ) ~~ B ) -> ( ( { (/) } X. A ) X. ( { 1o } X. B ) ) ~~ ( A X. B ) )
21 6 13 20 syl2an 
 |-  ( ( 1o ~< A /\ 1o ~< B ) -> ( ( { (/) } X. A ) X. ( { 1o } X. B ) ) ~~ ( A X. B ) )
22 domentr 
 |-  ( ( ( A |_| B ) ~<_ ( ( { (/) } X. A ) X. ( { 1o } X. B ) ) /\ ( ( { (/) } X. A ) X. ( { 1o } X. B ) ) ~~ ( A X. B ) ) -> ( A |_| B ) ~<_ ( A X. B ) )
23 19 21 22 syl2anc 
 |-  ( ( 1o ~< A /\ 1o ~< B ) -> ( A |_| B ) ~<_ ( A X. B ) )