# 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 ${⊢}{\phi }\to \left({x}\in {A}⟼{X}\right):{A}\underset{1-1 onto}{⟶}{B}$
xpf1o.2 ${⊢}{\phi }\to \left({y}\in {C}⟼{Y}\right):{C}\underset{1-1 onto}{⟶}{D}$
Assertion xpf1o ${⊢}{\phi }\to \left({x}\in {A},{y}\in {C}⟼⟨{X},{Y}⟩\right):{A}×{C}\underset{1-1 onto}{⟶}{B}×{D}$

### Proof

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