This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem unxpdom

Description: Cartesian product dominates union for sets with cardinality greater than 1. Proposition 10.36 of TakeutiZaring p. 93. (Contributed by Mario Carneiro, 13-Jan-2013) (Proof shortened by Mario Carneiro, 27-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 relsdom 
 |-  Rel ~<
2 1 brrelex2i 
 |-  ( 1o ~< A -> A e. _V )
3 1 brrelex2i 
 |-  ( 1o ~< B -> B e. _V )
4 2 3 anim12i 
 |-  ( ( 1o ~< A /\ 1o ~< B ) -> ( A e. _V /\ B e. _V ) )
5 breq2 
 |-  ( x = A -> ( 1o ~< x <-> 1o ~< A ) )
6 5 anbi1d 
 |-  ( x = A -> ( ( 1o ~< x /\ 1o ~< y ) <-> ( 1o ~< A /\ 1o ~< y ) ) )
7 uneq1 
 |-  ( x = A -> ( x u. y ) = ( A u. y ) )
8 xpeq1 
 |-  ( x = A -> ( x X. y ) = ( A X. y ) )
9 7 8 breq12d 
 |-  ( x = A -> ( ( x u. y ) ~<_ ( x X. y ) <-> ( A u. y ) ~<_ ( A X. y ) ) )
10 6 9 imbi12d 
 |-  ( x = A -> ( ( ( 1o ~< x /\ 1o ~< y ) -> ( x u. y ) ~<_ ( x X. y ) ) <-> ( ( 1o ~< A /\ 1o ~< y ) -> ( A u. y ) ~<_ ( A X. y ) ) ) )
11 breq2 
 |-  ( y = B -> ( 1o ~< y <-> 1o ~< B ) )
12 11 anbi2d 
 |-  ( y = B -> ( ( 1o ~< A /\ 1o ~< y ) <-> ( 1o ~< A /\ 1o ~< B ) ) )
13 uneq2 
 |-  ( y = B -> ( A u. y ) = ( A u. B ) )
14 xpeq2 
 |-  ( y = B -> ( A X. y ) = ( A X. B ) )
15 13 14 breq12d 
 |-  ( y = B -> ( ( A u. y ) ~<_ ( A X. y ) <-> ( A u. B ) ~<_ ( A X. B ) ) )
16 12 15 imbi12d 
 |-  ( y = B -> ( ( ( 1o ~< A /\ 1o ~< y ) -> ( A u. y ) ~<_ ( A X. y ) ) <-> ( ( 1o ~< A /\ 1o ~< B ) -> ( A u. B ) ~<_ ( A X. B ) ) ) )
17 eqid 
 |-  ( z e. ( x u. y ) |-> if ( z e. x , <. z , if ( z = v , w , t ) >. , <. if ( z = w , u , v ) , z >. ) ) = ( z e. ( x u. y ) |-> if ( z e. x , <. z , if ( z = v , w , t ) >. , <. if ( z = w , u , v ) , z >. ) )
18 eqid 
 |-  if ( z e. x , <. z , if ( z = v , w , t ) >. , <. if ( z = w , u , v ) , z >. ) = if ( z e. x , <. z , if ( z = v , w , t ) >. , <. if ( z = w , u , v ) , z >. )
19 17 18 unxpdomlem3 
 |-  ( ( 1o ~< x /\ 1o ~< y ) -> ( x u. y ) ~<_ ( x X. y ) )
20 10 16 19 vtocl2g 
 |-  ( ( A e. _V /\ B e. _V ) -> ( ( 1o ~< A /\ 1o ~< B ) -> ( A u. B ) ~<_ ( A X. B ) ) )
21 4 20 mpcom 
 |-  ( ( 1o ~< A /\ 1o ~< B ) -> ( A u. B ) ~<_ ( A X. B ) )