Metamath Proof Explorer

Theorem xpdom2

Description: Dominance law for Cartesian product. Proposition 10.33(2) of TakeutiZaring p. 92. (Contributed by NM, 24-Jul-2004) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Hypothesis xpdom.2 
|- C e. _V
Assertion xpdom2 
|- ( A ~<_ B -> ( C X. A ) ~<_ ( C X. B ) )

Proof

Step Hyp Ref Expression
1 xpdom.2 
 |-  C e. _V
2 brdomi 
 |-  ( A ~<_ B -> E. f f : A -1-1-> B )
3 f1f 
 |-  ( f : A -1-1-> B -> f : A --> B )
4 ffvelrn 
 |-  ( ( f : A --> B /\ U. ran { x } e. A ) -> ( f ` U. ran { x } ) e. B )
5 4 ex 
 |-  ( f : A --> B -> ( U. ran { x } e. A -> ( f ` U. ran { x } ) e. B ) )
6 3 5 syl 
 |-  ( f : A -1-1-> B -> ( U. ran { x } e. A -> ( f ` U. ran { x } ) e. B ) )
7 6 anim2d 
 |-  ( f : A -1-1-> B -> ( ( U. dom { x } e. C /\ U. ran { x } e. A ) -> ( U. dom { x } e. C /\ ( f ` U. ran { x } ) e. B ) ) )
8 7 adantld 
 |-  ( f : A -1-1-> B -> ( ( x = <. U. dom { x } , U. ran { x } >. /\ ( U. dom { x } e. C /\ U. ran { x } e. A ) ) -> ( U. dom { x } e. C /\ ( f ` U. ran { x } ) e. B ) ) )
9 elxp4 
 |-  ( x e. ( C X. A ) <-> ( x = <. U. dom { x } , U. ran { x } >. /\ ( U. dom { x } e. C /\ U. ran { x } e. A ) ) )
10 opelxp 
 |-  ( <. U. dom { x } , ( f ` U. ran { x } ) >. e. ( C X. B ) <-> ( U. dom { x } e. C /\ ( f ` U. ran { x } ) e. B ) )
11 8 9 10 3imtr4g 
 |-  ( f : A -1-1-> B -> ( x e. ( C X. A ) -> <. U. dom { x } , ( f ` U. ran { x } ) >. e. ( C X. B ) ) )
12 11 adantl 
 |-  ( ( A ~<_ B /\ f : A -1-1-> B ) -> ( x e. ( C X. A ) -> <. U. dom { x } , ( f ` U. ran { x } ) >. e. ( C X. B ) ) )
13 elxp2 
 |-  ( x e. ( C X. A ) <-> E. z e. C E. w e. A x = <. z , w >. )
14 elxp2 
 |-  ( y e. ( C X. A ) <-> E. v e. C E. u e. A y = <. v , u >. )
15 vex 
 |-  z e. _V
16 fvex 
 |-  ( f ` w ) e. _V
17 15 16 opth 
 |-  ( <. z , ( f ` w ) >. = <. v , ( f ` u ) >. <-> ( z = v /\ ( f ` w ) = ( f ` u ) ) )
18 f1fveq 
 |-  ( ( f : A -1-1-> B /\ ( w e. A /\ u e. A ) ) -> ( ( f ` w ) = ( f ` u ) <-> w = u ) )
19 18 ancoms 
 |-  ( ( ( w e. A /\ u e. A ) /\ f : A -1-1-> B ) -> ( ( f ` w ) = ( f ` u ) <-> w = u ) )
20 19 anbi2d 
 |-  ( ( ( w e. A /\ u e. A ) /\ f : A -1-1-> B ) -> ( ( z = v /\ ( f ` w ) = ( f ` u ) ) <-> ( z = v /\ w = u ) ) )
21 17 20 bitrid 
 |-  ( ( ( w e. A /\ u e. A ) /\ f : A -1-1-> B ) -> ( <. z , ( f ` w ) >. = <. v , ( f ` u ) >. <-> ( z = v /\ w = u ) ) )
22 21 ex 
 |-  ( ( w e. A /\ u e. A ) -> ( f : A -1-1-> B -> ( <. z , ( f ` w ) >. = <. v , ( f ` u ) >. <-> ( z = v /\ w = u ) ) ) )
23 22 ad2ant2l 
 |-  ( ( ( z e. C /\ w e. A ) /\ ( v e. C /\ u e. A ) ) -> ( f : A -1-1-> B -> ( <. z , ( f ` w ) >. = <. v , ( f ` u ) >. <-> ( z = v /\ w = u ) ) ) )
24 23 imp 
 |-  ( ( ( ( z e. C /\ w e. A ) /\ ( v e. C /\ u e. A ) ) /\ f : A -1-1-> B ) -> ( <. z , ( f ` w ) >. = <. v , ( f ` u ) >. <-> ( z = v /\ w = u ) ) )
25 24 adantlr 
 |-  ( ( ( ( ( z e. C /\ w e. A ) /\ ( v e. C /\ u e. A ) ) /\ ( x = <. z , w >. /\ y = <. v , u >. ) ) /\ f : A -1-1-> B ) -> ( <. z , ( f ` w ) >. = <. v , ( f ` u ) >. <-> ( z = v /\ w = u ) ) )
26 sneq 
 |-  ( x = <. z , w >. -> { x } = { <. z , w >. } )
27 26 dmeqd 
 |-  ( x = <. z , w >. -> dom { x } = dom { <. z , w >. } )
28 27 unieqd 
 |-  ( x = <. z , w >. -> U. dom { x } = U. dom { <. z , w >. } )
29 vex 
 |-  w e. _V
30 15 29 op1sta 
 |-  U. dom { <. z , w >. } = z
31 28 30 eqtrdi 
 |-  ( x = <. z , w >. -> U. dom { x } = z )
32 26 rneqd 
 |-  ( x = <. z , w >. -> ran { x } = ran { <. z , w >. } )
33 32 unieqd 
 |-  ( x = <. z , w >. -> U. ran { x } = U. ran { <. z , w >. } )
34 15 29 op2nda 
 |-  U. ran { <. z , w >. } = w
35 33 34 eqtrdi 
 |-  ( x = <. z , w >. -> U. ran { x } = w )
36 35 fveq2d 
 |-  ( x = <. z , w >. -> ( f ` U. ran { x } ) = ( f ` w ) )
37 31 36 opeq12d 
 |-  ( x = <. z , w >. -> <. U. dom { x } , ( f ` U. ran { x } ) >. = <. z , ( f ` w ) >. )
38 sneq 
 |-  ( y = <. v , u >. -> { y } = { <. v , u >. } )
39 38 dmeqd 
 |-  ( y = <. v , u >. -> dom { y } = dom { <. v , u >. } )
40 39 unieqd 
 |-  ( y = <. v , u >. -> U. dom { y } = U. dom { <. v , u >. } )
41 vex 
 |-  v e. _V
42 vex 
 |-  u e. _V
43 41 42 op1sta 
 |-  U. dom { <. v , u >. } = v
44 40 43 eqtrdi 
 |-  ( y = <. v , u >. -> U. dom { y } = v )
45 38 rneqd 
 |-  ( y = <. v , u >. -> ran { y } = ran { <. v , u >. } )
46 45 unieqd 
 |-  ( y = <. v , u >. -> U. ran { y } = U. ran { <. v , u >. } )
47 41 42 op2nda 
 |-  U. ran { <. v , u >. } = u
48 46 47 eqtrdi 
 |-  ( y = <. v , u >. -> U. ran { y } = u )
49 48 fveq2d 
 |-  ( y = <. v , u >. -> ( f ` U. ran { y } ) = ( f ` u ) )
50 44 49 opeq12d 
 |-  ( y = <. v , u >. -> <. U. dom { y } , ( f ` U. ran { y } ) >. = <. v , ( f ` u ) >. )
51 37 50 eqeqan12d 
 |-  ( ( x = <. z , w >. /\ y = <. v , u >. ) -> ( <. U. dom { x } , ( f ` U. ran { x } ) >. = <. U. dom { y } , ( f ` U. ran { y } ) >. <-> <. z , ( f ` w ) >. = <. v , ( f ` u ) >. ) )
52 51 ad2antlr 
 |-  ( ( ( ( ( z e. C /\ w e. A ) /\ ( v e. C /\ u e. A ) ) /\ ( x = <. z , w >. /\ y = <. v , u >. ) ) /\ f : A -1-1-> B ) -> ( <. U. dom { x } , ( f ` U. ran { x } ) >. = <. U. dom { y } , ( f ` U. ran { y } ) >. <-> <. z , ( f ` w ) >. = <. v , ( f ` u ) >. ) )
53 eqeq12 
 |-  ( ( x = <. z , w >. /\ y = <. v , u >. ) -> ( x = y <-> <. z , w >. = <. v , u >. ) )
54 15 29 opth 
 |-  ( <. z , w >. = <. v , u >. <-> ( z = v /\ w = u ) )
55 53 54 bitrdi 
 |-  ( ( x = <. z , w >. /\ y = <. v , u >. ) -> ( x = y <-> ( z = v /\ w = u ) ) )
56 55 ad2antlr 
 |-  ( ( ( ( ( z e. C /\ w e. A ) /\ ( v e. C /\ u e. A ) ) /\ ( x = <. z , w >. /\ y = <. v , u >. ) ) /\ f : A -1-1-> B ) -> ( x = y <-> ( z = v /\ w = u ) ) )
57 25 52 56 3bitr4d 
 |-  ( ( ( ( ( z e. C /\ w e. A ) /\ ( v e. C /\ u e. A ) ) /\ ( x = <. z , w >. /\ y = <. v , u >. ) ) /\ f : A -1-1-> B ) -> ( <. U. dom { x } , ( f ` U. ran { x } ) >. = <. U. dom { y } , ( f ` U. ran { y } ) >. <-> x = y ) )
58 57 exp53 
 |-  ( ( z e. C /\ w e. A ) -> ( ( v e. C /\ u e. A ) -> ( x = <. z , w >. -> ( y = <. v , u >. -> ( f : A -1-1-> B -> ( <. U. dom { x } , ( f ` U. ran { x } ) >. = <. U. dom { y } , ( f ` U. ran { y } ) >. <-> x = y ) ) ) ) ) )
59 58 com23 
 |-  ( ( z e. C /\ w e. A ) -> ( x = <. z , w >. -> ( ( v e. C /\ u e. A ) -> ( y = <. v , u >. -> ( f : A -1-1-> B -> ( <. U. dom { x } , ( f ` U. ran { x } ) >. = <. U. dom { y } , ( f ` U. ran { y } ) >. <-> x = y ) ) ) ) ) )
60 59 rexlimivv 
 |-  ( E. z e. C E. w e. A x = <. z , w >. -> ( ( v e. C /\ u e. A ) -> ( y = <. v , u >. -> ( f : A -1-1-> B -> ( <. U. dom { x } , ( f ` U. ran { x } ) >. = <. U. dom { y } , ( f ` U. ran { y } ) >. <-> x = y ) ) ) ) )
61 60 rexlimdvv 
 |-  ( E. z e. C E. w e. A x = <. z , w >. -> ( E. v e. C E. u e. A y = <. v , u >. -> ( f : A -1-1-> B -> ( <. U. dom { x } , ( f ` U. ran { x } ) >. = <. U. dom { y } , ( f ` U. ran { y } ) >. <-> x = y ) ) ) )
62 61 imp 
 |-  ( ( E. z e. C E. w e. A x = <. z , w >. /\ E. v e. C E. u e. A y = <. v , u >. ) -> ( f : A -1-1-> B -> ( <. U. dom { x } , ( f ` U. ran { x } ) >. = <. U. dom { y } , ( f ` U. ran { y } ) >. <-> x = y ) ) )
63 13 14 62 syl2anb 
 |-  ( ( x e. ( C X. A ) /\ y e. ( C X. A ) ) -> ( f : A -1-1-> B -> ( <. U. dom { x } , ( f ` U. ran { x } ) >. = <. U. dom { y } , ( f ` U. ran { y } ) >. <-> x = y ) ) )
64 63 com12 
 |-  ( f : A -1-1-> B -> ( ( x e. ( C X. A ) /\ y e. ( C X. A ) ) -> ( <. U. dom { x } , ( f ` U. ran { x } ) >. = <. U. dom { y } , ( f ` U. ran { y } ) >. <-> x = y ) ) )
65 64 adantl 
 |-  ( ( A ~<_ B /\ f : A -1-1-> B ) -> ( ( x e. ( C X. A ) /\ y e. ( C X. A ) ) -> ( <. U. dom { x } , ( f ` U. ran { x } ) >. = <. U. dom { y } , ( f ` U. ran { y } ) >. <-> x = y ) ) )
66 reldom 
 |-  Rel ~<_
67 66 brrelex1i 
 |-  ( A ~<_ B -> A e. _V )
68 xpexg 
 |-  ( ( C e. _V /\ A e. _V ) -> ( C X. A ) e. _V )
69 1 67 68 sylancr 
 |-  ( A ~<_ B -> ( C X. A ) e. _V )
70 69 adantr 
 |-  ( ( A ~<_ B /\ f : A -1-1-> B ) -> ( C X. A ) e. _V )
71 66 brrelex2i 
 |-  ( A ~<_ B -> B e. _V )
72 xpexg 
 |-  ( ( C e. _V /\ B e. _V ) -> ( C X. B ) e. _V )
73 1 71 72 sylancr 
 |-  ( A ~<_ B -> ( C X. B ) e. _V )
74 73 adantr 
 |-  ( ( A ~<_ B /\ f : A -1-1-> B ) -> ( C X. B ) e. _V )
75 12 65 70 74 dom3d 
 |-  ( ( A ~<_ B /\ f : A -1-1-> B ) -> ( C X. A ) ~<_ ( C X. B ) )
76 2 75 exlimddv 
 |-  ( A ~<_ B -> ( C X. A ) ~<_ ( C X. B ) )