Metamath Proof Explorer

Theorem xpwdomg

Description: Weak dominance of a Cartesian product. (Contributed by Stefan O'Rear, 13-Feb-2015) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Assertion xpwdomg 
|- ( ( A ~<_* B /\ C ~<_* D ) -> ( A X. C ) ~<_* ( B X. D ) )

Proof

Step Hyp Ref Expression
1 brwdom3i 
 |-  ( A ~<_* B -> E. f A. a e. A E. b e. B a = ( f ` b ) )
2 1 adantr 
 |-  ( ( A ~<_* B /\ C ~<_* D ) -> E. f A. a e. A E. b e. B a = ( f ` b ) )
3 brwdom3i 
 |-  ( C ~<_* D -> E. g A. c e. C E. d e. D c = ( g ` d ) )
4 3 adantl 
 |-  ( ( A ~<_* B /\ C ~<_* D ) -> E. g A. c e. C E. d e. D c = ( g ` d ) )
5 relwdom 
 |-  Rel ~<_*
6 5 brrelex1i 
 |-  ( A ~<_* B -> A e. _V )
7 5 brrelex1i 
 |-  ( C ~<_* D -> C e. _V )
8 xpexg 
 |-  ( ( A e. _V /\ C e. _V ) -> ( A X. C ) e. _V )
9 6 7 8 syl2an 
 |-  ( ( A ~<_* B /\ C ~<_* D ) -> ( A X. C ) e. _V )
10 9 adantr 
 |-  ( ( ( A ~<_* B /\ C ~<_* D ) /\ ( A. a e. A E. b e. B a = ( f ` b ) /\ A. c e. C E. d e. D c = ( g ` d ) ) ) -> ( A X. C ) e. _V )
11 5 brrelex2i 
 |-  ( A ~<_* B -> B e. _V )
12 5 brrelex2i 
 |-  ( C ~<_* D -> D e. _V )
13 xpexg 
 |-  ( ( B e. _V /\ D e. _V ) -> ( B X. D ) e. _V )
14 11 12 13 syl2an 
 |-  ( ( A ~<_* B /\ C ~<_* D ) -> ( B X. D ) e. _V )
15 14 adantr 
 |-  ( ( ( A ~<_* B /\ C ~<_* D ) /\ ( A. a e. A E. b e. B a = ( f ` b ) /\ A. c e. C E. d e. D c = ( g ` d ) ) ) -> ( B X. D ) e. _V )
16 pm3.2 
 |-  ( E. b e. B a = ( f ` b ) -> ( E. d e. D c = ( g ` d ) -> ( E. b e. B a = ( f ` b ) /\ E. d e. D c = ( g ` d ) ) ) )
17 16 ralimdv 
 |-  ( E. b e. B a = ( f ` b ) -> ( A. c e. C E. d e. D c = ( g ` d ) -> A. c e. C ( E. b e. B a = ( f ` b ) /\ E. d e. D c = ( g ` d ) ) ) )
18 17 com12 
 |-  ( A. c e. C E. d e. D c = ( g ` d ) -> ( E. b e. B a = ( f ` b ) -> A. c e. C ( E. b e. B a = ( f ` b ) /\ E. d e. D c = ( g ` d ) ) ) )
19 18 ralimdv 
 |-  ( A. c e. C E. d e. D c = ( g ` d ) -> ( A. a e. A E. b e. B a = ( f ` b ) -> A. a e. A A. c e. C ( E. b e. B a = ( f ` b ) /\ E. d e. D c = ( g ` d ) ) ) )
20 19 impcom 
 |-  ( ( A. a e. A E. b e. B a = ( f ` b ) /\ A. c e. C E. d e. D c = ( g ` d ) ) -> A. a e. A A. c e. C ( E. b e. B a = ( f ` b ) /\ E. d e. D c = ( g ` d ) ) )
21 pm3.2 
 |-  ( a = ( f ` b ) -> ( c = ( g ` d ) -> ( a = ( f ` b ) /\ c = ( g ` d ) ) ) )
22 21 reximdv 
 |-  ( a = ( f ` b ) -> ( E. d e. D c = ( g ` d ) -> E. d e. D ( a = ( f ` b ) /\ c = ( g ` d ) ) ) )
23 22 com12 
 |-  ( E. d e. D c = ( g ` d ) -> ( a = ( f ` b ) -> E. d e. D ( a = ( f ` b ) /\ c = ( g ` d ) ) ) )
24 23 reximdv 
 |-  ( E. d e. D c = ( g ` d ) -> ( E. b e. B a = ( f ` b ) -> E. b e. B E. d e. D ( a = ( f ` b ) /\ c = ( g ` d ) ) ) )
25 24 impcom 
 |-  ( ( E. b e. B a = ( f ` b ) /\ E. d e. D c = ( g ` d ) ) -> E. b e. B E. d e. D ( a = ( f ` b ) /\ c = ( g ` d ) ) )
26 25 2ralimi 
 |-  ( A. a e. A A. c e. C ( E. b e. B a = ( f ` b ) /\ E. d e. D c = ( g ` d ) ) -> A. a e. A A. c e. C E. b e. B E. d e. D ( a = ( f ` b ) /\ c = ( g ` d ) ) )
27 20 26 syl 
 |-  ( ( A. a e. A E. b e. B a = ( f ` b ) /\ A. c e. C E. d e. D c = ( g ` d ) ) -> A. a e. A A. c e. C E. b e. B E. d e. D ( a = ( f ` b ) /\ c = ( g ` d ) ) )
28 eqeq1 
 |-  ( x = <. a , c >. -> ( x = <. ( f ` b ) , ( g ` d ) >. <-> <. a , c >. = <. ( f ` b ) , ( g ` d ) >. ) )
29 vex 
 |-  a e. _V
30 vex 
 |-  c e. _V
31 29 30 opth 
 |-  ( <. a , c >. = <. ( f ` b ) , ( g ` d ) >. <-> ( a = ( f ` b ) /\ c = ( g ` d ) ) )
32 28 31 bitrdi 
 |-  ( x = <. a , c >. -> ( x = <. ( f ` b ) , ( g ` d ) >. <-> ( a = ( f ` b ) /\ c = ( g ` d ) ) ) )
33 32 2rexbidv 
 |-  ( x = <. a , c >. -> ( E. b e. B E. d e. D x = <. ( f ` b ) , ( g ` d ) >. <-> E. b e. B E. d e. D ( a = ( f ` b ) /\ c = ( g ` d ) ) ) )
34 33 ralxp 
 |-  ( A. x e. ( A X. C ) E. b e. B E. d e. D x = <. ( f ` b ) , ( g ` d ) >. <-> A. a e. A A. c e. C E. b e. B E. d e. D ( a = ( f ` b ) /\ c = ( g ` d ) ) )
35 27 34 sylibr 
 |-  ( ( A. a e. A E. b e. B a = ( f ` b ) /\ A. c e. C E. d e. D c = ( g ` d ) ) -> A. x e. ( A X. C ) E. b e. B E. d e. D x = <. ( f ` b ) , ( g ` d ) >. )
36 35 r19.21bi 
 |-  ( ( ( A. a e. A E. b e. B a = ( f ` b ) /\ A. c e. C E. d e. D c = ( g ` d ) ) /\ x e. ( A X. C ) ) -> E. b e. B E. d e. D x = <. ( f ` b ) , ( g ` d ) >. )
37 vex 
 |-  b e. _V
38 vex 
 |-  d e. _V
39 37 38 op1std 
 |-  ( y = <. b , d >. -> ( 1st ` y ) = b )
40 39 fveq2d 
 |-  ( y = <. b , d >. -> ( f ` ( 1st ` y ) ) = ( f ` b ) )
41 37 38 op2ndd 
 |-  ( y = <. b , d >. -> ( 2nd ` y ) = d )
42 41 fveq2d 
 |-  ( y = <. b , d >. -> ( g ` ( 2nd ` y ) ) = ( g ` d ) )
43 40 42 opeq12d 
 |-  ( y = <. b , d >. -> <. ( f ` ( 1st ` y ) ) , ( g ` ( 2nd ` y ) ) >. = <. ( f ` b ) , ( g ` d ) >. )
44 43 eqeq2d 
 |-  ( y = <. b , d >. -> ( x = <. ( f ` ( 1st ` y ) ) , ( g ` ( 2nd ` y ) ) >. <-> x = <. ( f ` b ) , ( g ` d ) >. ) )
45 44 rexxp 
 |-  ( E. y e. ( B X. D ) x = <. ( f ` ( 1st ` y ) ) , ( g ` ( 2nd ` y ) ) >. <-> E. b e. B E. d e. D x = <. ( f ` b ) , ( g ` d ) >. )
46 36 45 sylibr 
 |-  ( ( ( A. a e. A E. b e. B a = ( f ` b ) /\ A. c e. C E. d e. D c = ( g ` d ) ) /\ x e. ( A X. C ) ) -> E. y e. ( B X. D ) x = <. ( f ` ( 1st ` y ) ) , ( g ` ( 2nd ` y ) ) >. )
47 46 adantll 
 |-  ( ( ( ( A ~<_* B /\ C ~<_* D ) /\ ( A. a e. A E. b e. B a = ( f ` b ) /\ A. c e. C E. d e. D c = ( g ` d ) ) ) /\ x e. ( A X. C ) ) -> E. y e. ( B X. D ) x = <. ( f ` ( 1st ` y ) ) , ( g ` ( 2nd ` y ) ) >. )
48 10 15 47 wdom2d 
 |-  ( ( ( A ~<_* B /\ C ~<_* D ) /\ ( A. a e. A E. b e. B a = ( f ` b ) /\ A. c e. C E. d e. D c = ( g ` d ) ) ) -> ( A X. C ) ~<_* ( B X. D ) )
49 48 expr 
 |-  ( ( ( A ~<_* B /\ C ~<_* D ) /\ A. a e. A E. b e. B a = ( f ` b ) ) -> ( A. c e. C E. d e. D c = ( g ` d ) -> ( A X. C ) ~<_* ( B X. D ) ) )
50 49 exlimdv 
 |-  ( ( ( A ~<_* B /\ C ~<_* D ) /\ A. a e. A E. b e. B a = ( f ` b ) ) -> ( E. g A. c e. C E. d e. D c = ( g ` d ) -> ( A X. C ) ~<_* ( B X. D ) ) )
51 50 ex 
 |-  ( ( A ~<_* B /\ C ~<_* D ) -> ( A. a e. A E. b e. B a = ( f ` b ) -> ( E. g A. c e. C E. d e. D c = ( g ` d ) -> ( A X. C ) ~<_* ( B X. D ) ) ) )
52 51 exlimdv 
 |-  ( ( A ~<_* B /\ C ~<_* D ) -> ( E. f A. a e. A E. b e. B a = ( f ` b ) -> ( E. g A. c e. C E. d e. D c = ( g ` d ) -> ( A X. C ) ~<_* ( B X. D ) ) ) )
53 2 4 52 mp2d 
 |-  ( ( A ~<_* B /\ C ~<_* D ) -> ( A X. C ) ~<_* ( B X. D ) )