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 φ x A X : A 1-1 onto B
xpf1o.2 φ y C Y : C 1-1 onto D
Assertion xpf1o φ x A , y C X Y : A × C 1-1 onto B × D

Proof

Step Hyp Ref Expression
1 xpf1o.1 φ x A X : A 1-1 onto B
2 xpf1o.2 φ y C Y : C 1-1 onto D
3 xp1st u A × C 1 st u A
4 3 adantl φ u A × C 1 st u A
5 eqid x A X = x A X
6 5 f1ompt x A X : A 1-1 onto B x A X B z B ∃! x A z = X
7 1 6 sylib φ x A X B z B ∃! x A z = X
8 7 simpld φ x A X B
9 8 adantr φ u A × C x A X B
10 nfcsb1v _ x 1 st u / x X
11 10 nfel1 x 1 st u / x X B
12 csbeq1a x = 1 st u X = 1 st u / x X
13 12 eleq1d x = 1 st u X B 1 st u / x X B
14 11 13 rspc 1 st u A x A X B 1 st u / x X B
15 4 9 14 sylc φ u A × C 1 st u / x X B
16 xp2nd u A × C 2 nd u C
17 16 adantl φ u A × C 2 nd u C
18 eqid y C Y = y C Y
19 18 f1ompt y C Y : C 1-1 onto D y C Y D w D ∃! y C w = Y
20 2 19 sylib φ y C Y D w D ∃! y C w = Y
21 20 simpld φ y C Y D
22 21 adantr φ u A × C y C Y D
23 nfcsb1v _ y 2 nd u / y Y
24 23 nfel1 y 2 nd u / y Y D
25 csbeq1a y = 2 nd u Y = 2 nd u / y Y
26 25 eleq1d y = 2 nd u Y D 2 nd u / y Y D
27 24 26 rspc 2 nd u C y C Y D 2 nd u / y Y D
28 17 22 27 sylc φ u A × C 2 nd u / y Y D
29 15 28 opelxpd φ u A × C 1 st u / x X 2 nd u / y Y B × D
30 29 ralrimiva φ u A × C 1 st u / x X 2 nd u / y Y B × D
31 7 simprd φ z B ∃! x A z = X
32 31 r19.21bi φ z B ∃! x A z = X
33 reu6 ∃! x A z = X s A x A z = X x = s
34 32 33 sylib φ z B s A x A z = X x = s
35 20 simprd φ w D ∃! y C w = Y
36 35 r19.21bi φ w D ∃! y C w = Y
37 reu6 ∃! y C w = Y t C y C w = Y y = t
38 36 37 sylib φ w D t C y C w = Y y = t
39 34 38 anim12dan φ z B w D s A x A z = X x = s t C y C w = Y y = t
40 reeanv s A t C x A z = X x = s y C w = Y y = t s A x A z = X x = s t C y 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 y C w = Y y = t y C z = X w = Y x = s y = t
44 43 com12 y C w = Y y = t z = X x = s y C z = X w = Y x = s y = t
45 44 ralimdv y C w = Y y = t x A z = X x = s x A y C z = X w = Y x = s y = t
46 45 impcom x A z = X x = s y C w = Y y = t x A y C z = X w = Y x = s y = t
47 46 reximi t C x A z = X x = s y C w = Y y = t t C x A y C z = X w = Y x = s y = t
48 47 reximi s A t C x A z = X x = s y C w = Y y = t s A t C x A y C z = X w = Y x = s y = t
49 40 48 sylbir s A x A z = X x = s t C y C w = Y y = t s A t C x A y C z = X w = Y x = s y = t
50 39 49 syl φ z B w D s A t C x A y C z = X w = Y x = s y = t
51 vex s V
52 vex t V
53 51 52 op1std u = s t 1 st u = s
54 53 csbeq1d u = s t 1 st u / x X = s / x X
55 54 eqeq2d u = s t z = 1 st u / x X z = s / x X
56 51 52 op2ndd u = s t 2 nd u = t
57 56 csbeq1d u = s t 2 nd u / y Y = t / y Y
58 57 eqeq2d u = s t w = 2 nd u / y Y w = t / y Y
59 55 58 anbi12d u = s t z = 1 st u / x X w = 2 nd 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 = 1 st u / x X w = 2 nd u / y Y u = v z = s / x X w = t / y Y s t = v
62 61 ralxp u A × C z = 1 st u / x X w = 2 nd u / y Y u = v s A t C z = s / x X w = t / y Y s t = v
63 nfv s y C z = X w = Y x y = v
64 nfcv _ x C
65 nfcsb1v _ x s / x X
66 65 nfeq2 x z = s / x X
67 nfv x w = t / y Y
68 66 67 nfan x z = s / x X w = t / y Y
69 nfv x s t = v
70 68 69 nfbi x z = s / x X w = t / y Y s t = v
71 64 70 nfralw x t C z = s / x X w = t / y Y s t = v
72 nfv t z = X w = Y x y = v
73 nfv y z = X
74 nfcsb1v _ y t / y Y
75 74 nfeq2 y w = t / y Y
76 73 75 nfan y z = X w = t / y Y
77 nfv y x t = v
78 76 77 nfbi 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 y C z = X w = Y x y = v t 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 t C z = X w = t / y Y x t = v t C z = s / x X w = t / y Y s t = v
93 85 92 syl5bb x = s y C z = X w = Y x y = v t C z = s / x X w = t / y Y s t = v
94 63 71 93 cbvralw x A y C z = X w = Y x y = v s A t C z = s / x X w = t / y Y s t = v
95 62 94 bitr4i u A × C z = 1 st u / x X w = 2 nd u / y Y u = v x A y C z = X w = Y x y = v
96 eqeq2 v = s t x y = v x y = s t
97 vex x V
98 vex y 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 x A y C z = X w = Y x y = v x A y C z = X w = Y x = s y = t
103 95 102 syl5bb v = s t u A × C z = 1 st u / x X w = 2 nd u / y Y u = v x A y C z = X w = Y x = s y = t
104 103 rexxp v A × C u A × C z = 1 st u / x X w = 2 nd u / y Y u = v s A t C x A y C z = X w = Y x = s y = t
105 50 104 sylibr φ z B w D v A × C u A × C z = 1 st u / x X w = 2 nd u / y Y u = v
106 reu6 ∃! u A × C z = 1 st u / x X w = 2 nd u / y Y v A × C u A × C z = 1 st u / x X w = 2 nd u / y Y u = v
107 105 106 sylibr φ z B w D ∃! u A × C z = 1 st u / x X w = 2 nd u / y Y
108 107 ralrimivva φ z B w D ∃! u A × C z = 1 st u / x X w = 2 nd u / y Y
109 eqeq1 v = z w v = 1 st u / x X 2 nd u / y Y z w = 1 st u / x X 2 nd u / y Y
110 vex z V
111 vex w V
112 110 111 opth z w = 1 st u / x X 2 nd u / y Y z = 1 st u / x X w = 2 nd u / y Y
113 109 112 bitrdi v = z w v = 1 st u / x X 2 nd u / y Y z = 1 st u / x X w = 2 nd u / y Y
114 113 reubidv v = z w ∃! u A × C v = 1 st u / x X 2 nd u / y Y ∃! u A × C z = 1 st u / x X w = 2 nd u / y Y
115 114 ralxp v B × D ∃! u A × C v = 1 st u / x X 2 nd u / y Y z B w D ∃! u A × C z = 1 st u / x X w = 2 nd u / y Y
116 108 115 sylibr φ v B × D ∃! u A × C v = 1 st u / x X 2 nd u / y Y
117 nfcv _ z X Y
118 nfcv _ w X Y
119 nfcsb1v _ x z / x X
120 nfcv _ x w / y Y
121 119 120 nfop _ x z / x X w / y Y
122 nfcv _ y z / x X
123 nfcsb1v _ y w / y Y
124 122 123 nfop _ 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 A , y C X Y = z A , w C z / x X w / y Y
130 110 111 op1std u = z w 1 st u = z
131 130 csbeq1d u = z w 1 st u / x X = z / x X
132 110 111 op2ndd u = z w 2 nd u = w
133 132 csbeq1d u = z w 2 nd u / y Y = w / y Y
134 131 133 opeq12d u = z w 1 st u / x X 2 nd u / y Y = z / x X w / y Y
135 134 mpompt u A × C 1 st u / x X 2 nd u / y Y = z A , w C z / x X w / y Y
136 129 135 eqtr4i x A , y C X Y = u A × C 1 st u / x X 2 nd u / y Y
137 136 f1ompt x A , y C X Y : A × C 1-1 onto B × D u A × C 1 st u / x X 2 nd u / y Y B × D v B × D ∃! u A × C v = 1 st u / x X 2 nd u / y Y
138 30 116 137 sylanbrc φ x A , y C X Y : A × C 1-1 onto B × D