Metamath Proof Explorer

Theorem xpf1o

Description: Construct a bijection on a Cartesian product given bijections on the factors. (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Hypotheses xpf1o.1 
|- ( ph -> ( x e. A |-> X ) : A -1-1-onto-> B )
xpf1o.2 
|- ( ph -> ( y e. C |-> Y ) : C -1-1-onto-> D )
Assertion xpf1o 
|- ( ph -> ( x e. A , y e. C |-> <. X , Y >. ) : ( A X. C ) -1-1-onto-> ( B X. D ) )

Proof

Step Hyp Ref Expression
1 xpf1o.1 
 |-  ( ph -> ( x e. A |-> X ) : A -1-1-onto-> B )
2 xpf1o.2 
 |-  ( ph -> ( y e. C |-> Y ) : C -1-1-onto-> D )
3 xp1st 
 |-  ( u e. ( A X. C ) -> ( 1st ` u ) e. A )
4 3 adantl 
 |-  ( ( ph /\ u e. ( A X. C ) ) -> ( 1st ` u ) e. A )
5 eqid 
 |-  ( x e. A |-> X ) = ( x e. A |-> X )
6 5 f1ompt 
 |-  ( ( x e. A |-> X ) : A -1-1-onto-> B <-> ( A. x e. A X e. B /\ A. z e. B E! x e. A z = X ) )
7 1 6 sylib 
 |-  ( ph -> ( A. x e. A X e. B /\ A. z e. B E! x e. A z = X ) )
8 7 simpld 
 |-  ( ph -> A. x e. A X e. B )
9 8 adantr 
 |-  ( ( ph /\ u e. ( A X. C ) ) -> A. x e. A X e. B )
10 nfcsb1v 
 |-  F/_ x [_ ( 1st ` u ) / x ]_ X
11 10 nfel1 
 |-  F/ x [_ ( 1st ` u ) / x ]_ X e. B
12 csbeq1a 
 |-  ( x = ( 1st ` u ) -> X = [_ ( 1st ` u ) / x ]_ X )
13 12 eleq1d 
 |-  ( x = ( 1st ` u ) -> ( X e. B <-> [_ ( 1st ` u ) / x ]_ X e. B ) )
14 11 13 rspc 
 |-  ( ( 1st ` u ) e. A -> ( A. x e. A X e. B -> [_ ( 1st ` u ) / x ]_ X e. B ) )
15 4 9 14 sylc 
 |-  ( ( ph /\ u e. ( A X. C ) ) -> [_ ( 1st ` u ) / x ]_ X e. B )
16 xp2nd 
 |-  ( u e. ( A X. C ) -> ( 2nd ` u ) e. C )
17 16 adantl 
 |-  ( ( ph /\ u e. ( A X. C ) ) -> ( 2nd ` u ) e. C )
18 eqid 
 |-  ( y e. C |-> Y ) = ( y e. C |-> Y )
19 18 f1ompt 
 |-  ( ( y e. C |-> Y ) : C -1-1-onto-> D <-> ( A. y e. C Y e. D /\ A. w e. D E! y e. C w = Y ) )
20 2 19 sylib 
 |-  ( ph -> ( A. y e. C Y e. D /\ A. w e. D E! y e. C w = Y ) )
21 20 simpld 
 |-  ( ph -> A. y e. C Y e. D )
22 21 adantr 
 |-  ( ( ph /\ u e. ( A X. C ) ) -> A. y e. C Y e. D )
23 nfcsb1v 
 |-  F/_ y [_ ( 2nd ` u ) / y ]_ Y
24 23 nfel1 
 |-  F/ y [_ ( 2nd ` u ) / y ]_ Y e. D
25 csbeq1a 
 |-  ( y = ( 2nd ` u ) -> Y = [_ ( 2nd ` u ) / y ]_ Y )
26 25 eleq1d 
 |-  ( y = ( 2nd ` u ) -> ( Y e. D <-> [_ ( 2nd ` u ) / y ]_ Y e. D ) )
27 24 26 rspc 
 |-  ( ( 2nd ` u ) e. C -> ( A. y e. C Y e. D -> [_ ( 2nd ` u ) / y ]_ Y e. D ) )
28 17 22 27 sylc 
 |-  ( ( ph /\ u e. ( A X. C ) ) -> [_ ( 2nd ` u ) / y ]_ Y e. D )
29 15 28 opelxpd 
 |-  ( ( ph /\ u e. ( A X. C ) ) -> <. [_ ( 1st ` u ) / x ]_ X , [_ ( 2nd ` u ) / y ]_ Y >. e. ( B X. D ) )
30 29 ralrimiva 
 |-  ( ph -> A. u e. ( A X. C ) <. [_ ( 1st ` u ) / x ]_ X , [_ ( 2nd ` u ) / y ]_ Y >. e. ( B X. D ) )
31 7 simprd 
 |-  ( ph -> A. z e. B E! x e. A z = X )
32 31 r19.21bi 
 |-  ( ( ph /\ z e. B ) -> E! x e. A z = X )
33 reu6 
 |-  ( E! x e. A z = X <-> E. s e. A A. x e. A ( z = X <-> x = s ) )
34 32 33 sylib 
 |-  ( ( ph /\ z e. B ) -> E. s e. A A. x e. A ( z = X <-> x = s ) )
35 20 simprd 
 |-  ( ph -> A. w e. D E! y e. C w = Y )
36 35 r19.21bi 
 |-  ( ( ph /\ w e. D ) -> E! y e. C w = Y )
37 reu6 
 |-  ( E! y e. C w = Y <-> E. t e. C A. y e. C ( w = Y <-> y = t ) )
38 36 37 sylib 
 |-  ( ( ph /\ w e. D ) -> E. t e. C A. y e. C ( w = Y <-> y = t ) )
39 34 38 anim12dan 
 |-  ( ( ph /\ ( z e. B /\ w e. D ) ) -> ( E. s e. A A. x e. A ( z = X <-> x = s ) /\ E. t e. C A. y e. C ( w = Y <-> y = t ) ) )
40 reeanv 
 |-  ( E. s e. A E. t e. C ( A. x e. A ( z = X <-> x = s ) /\ A. y e. C ( w = Y <-> y = t ) ) <-> ( E. s e. A A. x e. A ( z = X <-> x = s ) /\ E. t e. C A. y e. C ( w = Y <-> y = t ) ) )
41 pm4.38 
 |-  ( ( ( z = X <-> x = s ) /\ ( w = Y <-> y = t ) ) -> ( ( z = X /\ w = Y ) <-> ( x = s /\ y = t ) ) )
42 41 ex 
 |-  ( ( z = X <-> x = s ) -> ( ( w = Y <-> y = t ) -> ( ( z = X /\ w = Y ) <-> ( x = s /\ y = t ) ) ) )
43 42 ralimdv 
 |-  ( ( z = X <-> x = s ) -> ( A. y e. C ( w = Y <-> y = t ) -> A. y e. C ( ( z = X /\ w = Y ) <-> ( x = s /\ y = t ) ) ) )
44 43 com12 
 |-  ( A. y e. C ( w = Y <-> y = t ) -> ( ( z = X <-> x = s ) -> A. y e. C ( ( z = X /\ w = Y ) <-> ( x = s /\ y = t ) ) ) )
45 44 ralimdv 
 |-  ( A. y e. C ( w = Y <-> y = t ) -> ( A. x e. A ( z = X <-> x = s ) -> A. x e. A A. y e. C ( ( z = X /\ w = Y ) <-> ( x = s /\ y = t ) ) ) )
46 45 impcom 
 |-  ( ( A. x e. A ( z = X <-> x = s ) /\ A. y e. C ( w = Y <-> y = t ) ) -> A. x e. A A. y e. C ( ( z = X /\ w = Y ) <-> ( x = s /\ y = t ) ) )
47 46 reximi 
 |-  ( E. t e. C ( A. x e. A ( z = X <-> x = s ) /\ A. y e. C ( w = Y <-> y = t ) ) -> E. t e. C A. x e. A A. y e. C ( ( z = X /\ w = Y ) <-> ( x = s /\ y = t ) ) )
48 47 reximi 
 |-  ( E. s e. A E. t e. C ( A. x e. A ( z = X <-> x = s ) /\ A. y e. C ( w = Y <-> y = t ) ) -> E. s e. A E. t e. C A. x e. A A. y e. C ( ( z = X /\ w = Y ) <-> ( x = s /\ y = t ) ) )
49 40 48 sylbir 
 |-  ( ( E. s e. A A. x e. A ( z = X <-> x = s ) /\ E. t e. C A. y e. C ( w = Y <-> y = t ) ) -> E. s e. A E. t e. C A. x e. A A. y e. C ( ( z = X /\ w = Y ) <-> ( x = s /\ y = t ) ) )
50 39 49 syl 
 |-  ( ( ph /\ ( z e. B /\ w e. D ) ) -> E. s e. A E. t e. C A. x e. A A. y e. C ( ( z = X /\ w = Y ) <-> ( x = s /\ y = t ) ) )
51 vex 
 |-  s e. _V
52 vex 
 |-  t e. _V
53 51 52 op1std 
 |-  ( u = <. s , t >. -> ( 1st ` u ) = s )
54 53 csbeq1d 
 |-  ( u = <. s , t >. -> [_ ( 1st ` u ) / x ]_ X = [_ s / x ]_ X )
55 54 eqeq2d 
 |-  ( u = <. s , t >. -> ( z = [_ ( 1st ` u ) / x ]_ X <-> z = [_ s / x ]_ X ) )
56 51 52 op2ndd 
 |-  ( u = <. s , t >. -> ( 2nd ` u ) = t )
57 56 csbeq1d 
 |-  ( u = <. s , t >. -> [_ ( 2nd ` u ) / y ]_ Y = [_ t / y ]_ Y )
58 57 eqeq2d 
 |-  ( u = <. s , t >. -> ( w = [_ ( 2nd ` u ) / y ]_ Y <-> w = [_ t / y ]_ Y ) )
59 55 58 anbi12d 
 |-  ( u = <. s , t >. -> ( ( z = [_ ( 1st ` u ) / x ]_ X /\ w = [_ ( 2nd ` u ) / y ]_ Y ) <-> ( z = [_ s / x ]_ X /\ w = [_ t / y ]_ Y ) ) )
60 eqeq1 
 |-  ( u = <. s , t >. -> ( u = v <-> <. s , t >. = v ) )
61 59 60 bibi12d 
 |-  ( u = <. s , t >. -> ( ( ( z = [_ ( 1st ` u ) / x ]_ X /\ w = [_ ( 2nd ` u ) / y ]_ Y ) <-> u = v ) <-> ( ( z = [_ s / x ]_ X /\ w = [_ t / y ]_ Y ) <-> <. s , t >. = v ) ) )
62 61 ralxp 
 |-  ( A. u e. ( A X. C ) ( ( z = [_ ( 1st ` u ) / x ]_ X /\ w = [_ ( 2nd ` u ) / y ]_ Y ) <-> u = v ) <-> A. s e. A A. t e. C ( ( z = [_ s / x ]_ X /\ w = [_ t / y ]_ Y ) <-> <. s , t >. = v ) )
63 nfv 
 |-  F/ s A. y e. C ( ( z = X /\ w = Y ) <-> <. x , y >. = v )
64 nfcv 
 |-  F/_ x C
65 nfcsb1v 
 |-  F/_ x [_ s / x ]_ X
66 65 nfeq2 
 |-  F/ x z = [_ s / x ]_ X
67 nfv 
 |-  F/ x w = [_ t / y ]_ Y
68 66 67 nfan 
 |-  F/ x ( z = [_ s / x ]_ X /\ w = [_ t / y ]_ Y )
69 nfv 
 |-  F/ x <. s , t >. = v
70 68 69 nfbi 
 |-  F/ x ( ( z = [_ s / x ]_ X /\ w = [_ t / y ]_ Y ) <-> <. s , t >. = v )
71 64 70 nfralw 
 |-  F/ x A. t e. C ( ( z = [_ s / x ]_ X /\ w = [_ t / y ]_ Y ) <-> <. s , t >. = v )
72 nfv 
 |-  F/ t ( ( z = X /\ w = Y ) <-> <. x , y >. = v )
73 nfv 
 |-  F/ y z = X
74 nfcsb1v 
 |-  F/_ y [_ t / y ]_ Y
75 74 nfeq2 
 |-  F/ y w = [_ t / y ]_ Y
76 73 75 nfan 
 |-  F/ y ( z = X /\ w = [_ t / y ]_ Y )
77 nfv 
 |-  F/ y <. x , t >. = v
78 76 77 nfbi 
 |-  F/ y ( ( z = X /\ w = [_ t / y ]_ Y ) <-> <. x , t >. = v )
79 csbeq1a 
 |-  ( y = t -> Y = [_ t / y ]_ Y )
80 79 eqeq2d 
 |-  ( y = t -> ( w = Y <-> w = [_ t / y ]_ Y ) )
81 80 anbi2d 
 |-  ( y = t -> ( ( z = X /\ w = Y ) <-> ( z = X /\ w = [_ t / y ]_ Y ) ) )
82 opeq2 
 |-  ( y = t -> <. x , y >. = <. x , t >. )
83 82 eqeq1d 
 |-  ( y = t -> ( <. x , y >. = v <-> <. x , t >. = v ) )
84 81 83 bibi12d 
 |-  ( y = t -> ( ( ( z = X /\ w = Y ) <-> <. x , y >. = v ) <-> ( ( z = X /\ w = [_ t / y ]_ Y ) <-> <. x , t >. = v ) ) )
85 72 78 84 cbvralw 
 |-  ( A. y e. C ( ( z = X /\ w = Y ) <-> <. x , y >. = v ) <-> A. t e. C ( ( z = X /\ w = [_ t / y ]_ Y ) <-> <. x , t >. = v ) )
86 csbeq1a 
 |-  ( x = s -> X = [_ s / x ]_ X )
87 86 eqeq2d 
 |-  ( x = s -> ( z = X <-> z = [_ s / x ]_ X ) )
88 87 anbi1d 
 |-  ( x = s -> ( ( z = X /\ w = [_ t / y ]_ Y ) <-> ( z = [_ s / x ]_ X /\ w = [_ t / y ]_ Y ) ) )
89 opeq1 
 |-  ( x = s -> <. x , t >. = <. s , t >. )
90 89 eqeq1d 
 |-  ( x = s -> ( <. x , t >. = v <-> <. s , t >. = v ) )
91 88 90 bibi12d 
 |-  ( x = s -> ( ( ( z = X /\ w = [_ t / y ]_ Y ) <-> <. x , t >. = v ) <-> ( ( z = [_ s / x ]_ X /\ w = [_ t / y ]_ Y ) <-> <. s , t >. = v ) ) )
92 91 ralbidv 
 |-  ( x = s -> ( A. t e. C ( ( z = X /\ w = [_ t / y ]_ Y ) <-> <. x , t >. = v ) <-> A. t e. C ( ( z = [_ s / x ]_ X /\ w = [_ t / y ]_ Y ) <-> <. s , t >. = v ) ) )
93 85 92 syl5bb 
 |-  ( x = s -> ( A. y e. C ( ( z = X /\ w = Y ) <-> <. x , y >. = v ) <-> A. t e. C ( ( z = [_ s / x ]_ X /\ w = [_ t / y ]_ Y ) <-> <. s , t >. = v ) ) )
94 63 71 93 cbvralw 
 |-  ( A. x e. A A. y e. C ( ( z = X /\ w = Y ) <-> <. x , y >. = v ) <-> A. s e. A A. t e. C ( ( z = [_ s / x ]_ X /\ w = [_ t / y ]_ Y ) <-> <. s , t >. = v ) )
95 62 94 bitr4i 
 |-  ( A. u e. ( A X. C ) ( ( z = [_ ( 1st ` u ) / x ]_ X /\ w = [_ ( 2nd ` u ) / y ]_ Y ) <-> u = v ) <-> A. x e. A A. y e. C ( ( z = X /\ w = Y ) <-> <. x , y >. = v ) )
96 eqeq2 
 |-  ( v = <. s , t >. -> ( <. x , y >. = v <-> <. x , y >. = <. s , t >. ) )
97 vex 
 |-  x e. _V
98 vex 
 |-  y e. _V
99 97 98 opth 
 |-  ( <. x , y >. = <. s , t >. <-> ( x = s /\ y = t ) )
100 96 99 bitrdi 
 |-  ( v = <. s , t >. -> ( <. x , y >. = v <-> ( x = s /\ y = t ) ) )
101 100 bibi2d 
 |-  ( v = <. s , t >. -> ( ( ( z = X /\ w = Y ) <-> <. x , y >. = v ) <-> ( ( z = X /\ w = Y ) <-> ( x = s /\ y = t ) ) ) )
102 101 2ralbidv 
 |-  ( v = <. s , t >. -> ( A. x e. A A. y e. C ( ( z = X /\ w = Y ) <-> <. x , y >. = v ) <-> A. x e. A A. y e. C ( ( z = X /\ w = Y ) <-> ( x = s /\ y = t ) ) ) )
103 95 102 syl5bb 
 |-  ( v = <. s , t >. -> ( A. u e. ( A X. C ) ( ( z = [_ ( 1st ` u ) / x ]_ X /\ w = [_ ( 2nd ` u ) / y ]_ Y ) <-> u = v ) <-> A. x e. A A. y e. C ( ( z = X /\ w = Y ) <-> ( x = s /\ y = t ) ) ) )
104 103 rexxp 
 |-  ( E. v e. ( A X. C ) A. u e. ( A X. C ) ( ( z = [_ ( 1st ` u ) / x ]_ X /\ w = [_ ( 2nd ` u ) / y ]_ Y ) <-> u = v ) <-> E. s e. A E. t e. C A. x e. A A. y e. C ( ( z = X /\ w = Y ) <-> ( x = s /\ y = t ) ) )
105 50 104 sylibr 
 |-  ( ( ph /\ ( z e. B /\ w e. D ) ) -> E. v e. ( A X. C ) A. u e. ( A X. C ) ( ( z = [_ ( 1st ` u ) / x ]_ X /\ w = [_ ( 2nd ` u ) / y ]_ Y ) <-> u = v ) )
106 reu6 
 |-  ( E! u e. ( A X. C ) ( z = [_ ( 1st ` u ) / x ]_ X /\ w = [_ ( 2nd ` u ) / y ]_ Y ) <-> E. v e. ( A X. C ) A. u e. ( A X. C ) ( ( z = [_ ( 1st ` u ) / x ]_ X /\ w = [_ ( 2nd ` u ) / y ]_ Y ) <-> u = v ) )
107 105 106 sylibr 
 |-  ( ( ph /\ ( z e. B /\ w e. D ) ) -> E! u e. ( A X. C ) ( z = [_ ( 1st ` u ) / x ]_ X /\ w = [_ ( 2nd ` u ) / y ]_ Y ) )
108 107 ralrimivva 
 |-  ( ph -> A. z e. B A. w e. D E! u e. ( A X. C ) ( z = [_ ( 1st ` u ) / x ]_ X /\ w = [_ ( 2nd ` u ) / y ]_ Y ) )
109 eqeq1 
 |-  ( v = <. z , w >. -> ( v = <. [_ ( 1st ` u ) / x ]_ X , [_ ( 2nd ` u ) / y ]_ Y >. <-> <. z , w >. = <. [_ ( 1st ` u ) / x ]_ X , [_ ( 2nd ` u ) / y ]_ Y >. ) )
110 vex 
 |-  z e. _V
111 vex 
 |-  w e. _V
112 110 111 opth 
 |-  ( <. z , w >. = <. [_ ( 1st ` u ) / x ]_ X , [_ ( 2nd ` u ) / y ]_ Y >. <-> ( z = [_ ( 1st ` u ) / x ]_ X /\ w = [_ ( 2nd ` u ) / y ]_ Y ) )
113 109 112 bitrdi 
 |-  ( v = <. z , w >. -> ( v = <. [_ ( 1st ` u ) / x ]_ X , [_ ( 2nd ` u ) / y ]_ Y >. <-> ( z = [_ ( 1st ` u ) / x ]_ X /\ w = [_ ( 2nd ` u ) / y ]_ Y ) ) )
114 113 reubidv 
 |-  ( v = <. z , w >. -> ( E! u e. ( A X. C ) v = <. [_ ( 1st ` u ) / x ]_ X , [_ ( 2nd ` u ) / y ]_ Y >. <-> E! u e. ( A X. C ) ( z = [_ ( 1st ` u ) / x ]_ X /\ w = [_ ( 2nd ` u ) / y ]_ Y ) ) )
115 114 ralxp 
 |-  ( A. v e. ( B X. D ) E! u e. ( A X. C ) v = <. [_ ( 1st ` u ) / x ]_ X , [_ ( 2nd ` u ) / y ]_ Y >. <-> A. z e. B A. w e. D E! u e. ( A X. C ) ( z = [_ ( 1st ` u ) / x ]_ X /\ w = [_ ( 2nd ` u ) / y ]_ Y ) )
116 108 115 sylibr 
 |-  ( ph -> A. v e. ( B X. D ) E! u e. ( A X. C ) v = <. [_ ( 1st ` u ) / x ]_ X , [_ ( 2nd ` u ) / y ]_ Y >. )
117 nfcv 
 |-  F/_ z <. X , Y >.
118 nfcv 
 |-  F/_ w <. X , Y >.
119 nfcsb1v 
 |-  F/_ x [_ z / x ]_ X
120 nfcv 
 |-  F/_ x [_ w / y ]_ Y
121 119 120 nfop 
 |-  F/_ x <. [_ z / x ]_ X , [_ w / y ]_ Y >.
122 nfcv 
 |-  F/_ y [_ z / x ]_ X
123 nfcsb1v 
 |-  F/_ y [_ w / y ]_ Y
124 122 123 nfop 
 |-  F/_ y <. [_ z / x ]_ X , [_ w / y ]_ Y >.
125 csbeq1a 
 |-  ( x = z -> X = [_ z / x ]_ X )
126 csbeq1a 
 |-  ( y = w -> Y = [_ w / y ]_ Y )
127 opeq12 
 |-  ( ( X = [_ z / x ]_ X /\ Y = [_ w / y ]_ Y ) -> <. X , Y >. = <. [_ z / x ]_ X , [_ w / y ]_ Y >. )
128 125 126 127 syl2an 
 |-  ( ( x = z /\ y = w ) -> <. X , Y >. = <. [_ z / x ]_ X , [_ w / y ]_ Y >. )
129 117 118 121 124 128 cbvmpo 
 |-  ( x e. A , y e. C |-> <. X , Y >. ) = ( z e. A , w e. C |-> <. [_ z / x ]_ X , [_ w / y ]_ Y >. )
130 110 111 op1std 
 |-  ( u = <. z , w >. -> ( 1st ` u ) = z )
131 130 csbeq1d 
 |-  ( u = <. z , w >. -> [_ ( 1st ` u ) / x ]_ X = [_ z / x ]_ X )
132 110 111 op2ndd 
 |-  ( u = <. z , w >. -> ( 2nd ` u ) = w )
133 132 csbeq1d 
 |-  ( u = <. z , w >. -> [_ ( 2nd ` u ) / y ]_ Y = [_ w / y ]_ Y )
134 131 133 opeq12d 
 |-  ( u = <. z , w >. -> <. [_ ( 1st ` u ) / x ]_ X , [_ ( 2nd ` u ) / y ]_ Y >. = <. [_ z / x ]_ X , [_ w / y ]_ Y >. )
135 134 mpompt 
 |-  ( u e. ( A X. C ) |-> <. [_ ( 1st ` u ) / x ]_ X , [_ ( 2nd ` u ) / y ]_ Y >. ) = ( z e. A , w e. C |-> <. [_ z / x ]_ X , [_ w / y ]_ Y >. )
136 129 135 eqtr4i 
 |-  ( x e. A , y e. C |-> <. X , Y >. ) = ( u e. ( A X. C ) |-> <. [_ ( 1st ` u ) / x ]_ X , [_ ( 2nd ` u ) / y ]_ Y >. )
137 136 f1ompt 
 |-  ( ( x e. A , y e. C |-> <. X , Y >. ) : ( A X. C ) -1-1-onto-> ( B X. D ) <-> ( A. u e. ( A X. C ) <. [_ ( 1st ` u ) / x ]_ X , [_ ( 2nd ` u ) / y ]_ Y >. e. ( B X. D ) /\ A. v e. ( B X. D ) E! u e. ( A X. C ) v = <. [_ ( 1st ` u ) / x ]_ X , [_ ( 2nd ` u ) / y ]_ Y >. ) )
138 30 116 137 sylanbrc 
 |-  ( ph -> ( x e. A , y e. C |-> <. X , Y >. ) : ( A X. C ) -1-1-onto-> ( B X. D ) )