# Metamath Proof Explorer

## Theorem xpsff1o

Description: The function appearing in xpsval is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = { (/) , 1o } . (Contributed by Mario Carneiro, 15-Aug-2015)

Ref Expression
Hypothesis xpsff1o.f ${⊢}{F}=\left({x}\in {A},{y}\in {B}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)$
Assertion xpsff1o ${⊢}{F}:{A}×{B}\underset{1-1 onto}{⟶}\underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)$

### Proof

Step Hyp Ref Expression
1 xpsff1o.f ${⊢}{F}=\left({x}\in {A},{y}\in {B}⟼\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\right)$
2 xpsfrnel2 ${⊢}\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)↔\left({x}\in {A}\wedge {y}\in {B}\right)$
3 2 biimpri ${⊢}\left({x}\in {A}\wedge {y}\in {B}\right)\to \left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)$
4 3 rgen2 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)$
5 1 fmpo ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left\{⟨\varnothing ,{x}⟩,⟨{1}_{𝑜},{y}⟩\right\}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)↔{F}:{A}×{B}⟶\underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)$
6 4 5 mpbi ${⊢}{F}:{A}×{B}⟶\underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)$
7 1st2nd2 ${⊢}{z}\in \left({A}×{B}\right)\to {z}=⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩$
8 7 fveq2d ${⊢}{z}\in \left({A}×{B}\right)\to {F}\left({z}\right)={F}\left(⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩\right)$
9 df-ov ${⊢}{1}^{st}\left({z}\right){F}{2}^{nd}\left({z}\right)={F}\left(⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩\right)$
10 xp1st ${⊢}{z}\in \left({A}×{B}\right)\to {1}^{st}\left({z}\right)\in {A}$
11 xp2nd ${⊢}{z}\in \left({A}×{B}\right)\to {2}^{nd}\left({z}\right)\in {B}$
12 1 xpsfval ${⊢}\left({1}^{st}\left({z}\right)\in {A}\wedge {2}^{nd}\left({z}\right)\in {B}\right)\to {1}^{st}\left({z}\right){F}{2}^{nd}\left({z}\right)=\left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}$
13 10 11 12 syl2anc ${⊢}{z}\in \left({A}×{B}\right)\to {1}^{st}\left({z}\right){F}{2}^{nd}\left({z}\right)=\left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}$
14 9 13 syl5eqr ${⊢}{z}\in \left({A}×{B}\right)\to {F}\left(⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩\right)=\left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}$
15 8 14 eqtrd ${⊢}{z}\in \left({A}×{B}\right)\to {F}\left({z}\right)=\left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}$
16 1st2nd2 ${⊢}{w}\in \left({A}×{B}\right)\to {w}=⟨{1}^{st}\left({w}\right),{2}^{nd}\left({w}\right)⟩$
17 16 fveq2d ${⊢}{w}\in \left({A}×{B}\right)\to {F}\left({w}\right)={F}\left(⟨{1}^{st}\left({w}\right),{2}^{nd}\left({w}\right)⟩\right)$
18 df-ov ${⊢}{1}^{st}\left({w}\right){F}{2}^{nd}\left({w}\right)={F}\left(⟨{1}^{st}\left({w}\right),{2}^{nd}\left({w}\right)⟩\right)$
19 xp1st ${⊢}{w}\in \left({A}×{B}\right)\to {1}^{st}\left({w}\right)\in {A}$
20 xp2nd ${⊢}{w}\in \left({A}×{B}\right)\to {2}^{nd}\left({w}\right)\in {B}$
21 1 xpsfval ${⊢}\left({1}^{st}\left({w}\right)\in {A}\wedge {2}^{nd}\left({w}\right)\in {B}\right)\to {1}^{st}\left({w}\right){F}{2}^{nd}\left({w}\right)=\left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}$
22 19 20 21 syl2anc ${⊢}{w}\in \left({A}×{B}\right)\to {1}^{st}\left({w}\right){F}{2}^{nd}\left({w}\right)=\left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}$
23 18 22 syl5eqr ${⊢}{w}\in \left({A}×{B}\right)\to {F}\left(⟨{1}^{st}\left({w}\right),{2}^{nd}\left({w}\right)⟩\right)=\left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}$
24 17 23 eqtrd ${⊢}{w}\in \left({A}×{B}\right)\to {F}\left({w}\right)=\left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}$
25 15 24 eqeqan12d ${⊢}\left({z}\in \left({A}×{B}\right)\wedge {w}\in \left({A}×{B}\right)\right)\to \left({F}\left({z}\right)={F}\left({w}\right)↔\left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}=\left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}\right)$
26 fveq1 ${⊢}\left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}=\left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}\to \left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}\left(\varnothing \right)=\left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}\left(\varnothing \right)$
27 fvex ${⊢}{1}^{st}\left({z}\right)\in \mathrm{V}$
28 fvpr0o ${⊢}{1}^{st}\left({z}\right)\in \mathrm{V}\to \left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}\left(\varnothing \right)={1}^{st}\left({z}\right)$
29 27 28 ax-mp ${⊢}\left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}\left(\varnothing \right)={1}^{st}\left({z}\right)$
30 fvex ${⊢}{1}^{st}\left({w}\right)\in \mathrm{V}$
31 fvpr0o ${⊢}{1}^{st}\left({w}\right)\in \mathrm{V}\to \left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}\left(\varnothing \right)={1}^{st}\left({w}\right)$
32 30 31 ax-mp ${⊢}\left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}\left(\varnothing \right)={1}^{st}\left({w}\right)$
33 26 29 32 3eqtr3g ${⊢}\left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}=\left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}\to {1}^{st}\left({z}\right)={1}^{st}\left({w}\right)$
34 fveq1 ${⊢}\left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}=\left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}\to \left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}\left({1}_{𝑜}\right)=\left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}\left({1}_{𝑜}\right)$
35 fvex ${⊢}{2}^{nd}\left({z}\right)\in \mathrm{V}$
36 fvpr1o ${⊢}{2}^{nd}\left({z}\right)\in \mathrm{V}\to \left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}\left({1}_{𝑜}\right)={2}^{nd}\left({z}\right)$
37 35 36 ax-mp ${⊢}\left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}\left({1}_{𝑜}\right)={2}^{nd}\left({z}\right)$
38 fvex ${⊢}{2}^{nd}\left({w}\right)\in \mathrm{V}$
39 fvpr1o ${⊢}{2}^{nd}\left({w}\right)\in \mathrm{V}\to \left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}\left({1}_{𝑜}\right)={2}^{nd}\left({w}\right)$
40 38 39 ax-mp ${⊢}\left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}\left({1}_{𝑜}\right)={2}^{nd}\left({w}\right)$
41 34 37 40 3eqtr3g ${⊢}\left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}=\left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}\to {2}^{nd}\left({z}\right)={2}^{nd}\left({w}\right)$
42 33 41 opeq12d ${⊢}\left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}=\left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}\to ⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩=⟨{1}^{st}\left({w}\right),{2}^{nd}\left({w}\right)⟩$
43 7 16 eqeqan12d ${⊢}\left({z}\in \left({A}×{B}\right)\wedge {w}\in \left({A}×{B}\right)\right)\to \left({z}={w}↔⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩=⟨{1}^{st}\left({w}\right),{2}^{nd}\left({w}\right)⟩\right)$
44 42 43 syl5ibr ${⊢}\left({z}\in \left({A}×{B}\right)\wedge {w}\in \left({A}×{B}\right)\right)\to \left(\left\{⟨\varnothing ,{1}^{st}\left({z}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({z}\right)⟩\right\}=\left\{⟨\varnothing ,{1}^{st}\left({w}\right)⟩,⟨{1}_{𝑜},{2}^{nd}\left({w}\right)⟩\right\}\to {z}={w}\right)$
45 25 44 sylbid ${⊢}\left({z}\in \left({A}×{B}\right)\wedge {w}\in \left({A}×{B}\right)\right)\to \left({F}\left({z}\right)={F}\left({w}\right)\to {z}={w}\right)$
46 45 rgen2 ${⊢}\forall {z}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}\left({F}\left({z}\right)={F}\left({w}\right)\to {z}={w}\right)$
47 dff13 ${⊢}{F}:{A}×{B}\underset{1-1}{⟶}\underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)↔\left({F}:{A}×{B}⟶\underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)\wedge \forall {z}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}\forall {w}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}\left({F}\left({z}\right)={F}\left({w}\right)\to {z}={w}\right)\right)$
48 6 46 47 mpbir2an ${⊢}{F}:{A}×{B}\underset{1-1}{⟶}\underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)$
49 xpsfrnel ${⊢}{z}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)↔\left({z}Fn{2}_{𝑜}\wedge {z}\left(\varnothing \right)\in {A}\wedge {z}\left({1}_{𝑜}\right)\in {B}\right)$
50 49 simp2bi ${⊢}{z}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)\to {z}\left(\varnothing \right)\in {A}$
51 49 simp3bi ${⊢}{z}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)\to {z}\left({1}_{𝑜}\right)\in {B}$
52 1 xpsfval ${⊢}\left({z}\left(\varnothing \right)\in {A}\wedge {z}\left({1}_{𝑜}\right)\in {B}\right)\to {z}\left(\varnothing \right){F}{z}\left({1}_{𝑜}\right)=\left\{⟨\varnothing ,{z}\left(\varnothing \right)⟩,⟨{1}_{𝑜},{z}\left({1}_{𝑜}\right)⟩\right\}$
53 50 51 52 syl2anc ${⊢}{z}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)\to {z}\left(\varnothing \right){F}{z}\left({1}_{𝑜}\right)=\left\{⟨\varnothing ,{z}\left(\varnothing \right)⟩,⟨{1}_{𝑜},{z}\left({1}_{𝑜}\right)⟩\right\}$
54 ixpfn ${⊢}{z}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)\to {z}Fn{2}_{𝑜}$
55 xpsfeq ${⊢}{z}Fn{2}_{𝑜}\to \left\{⟨\varnothing ,{z}\left(\varnothing \right)⟩,⟨{1}_{𝑜},{z}\left({1}_{𝑜}\right)⟩\right\}={z}$
56 54 55 syl ${⊢}{z}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)\to \left\{⟨\varnothing ,{z}\left(\varnothing \right)⟩,⟨{1}_{𝑜},{z}\left({1}_{𝑜}\right)⟩\right\}={z}$
57 53 56 eqtr2d ${⊢}{z}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)\to {z}={z}\left(\varnothing \right){F}{z}\left({1}_{𝑜}\right)$
58 rspceov ${⊢}\left({z}\left(\varnothing \right)\in {A}\wedge {z}\left({1}_{𝑜}\right)\in {B}\wedge {z}={z}\left(\varnothing \right){F}{z}\left({1}_{𝑜}\right)\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\exists {b}\in {B}\phantom{\rule{.4em}{0ex}}{z}={a}{F}{b}$
59 50 51 57 58 syl3anc ${⊢}{z}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)\to \exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\exists {b}\in {B}\phantom{\rule{.4em}{0ex}}{z}={a}{F}{b}$
60 59 rgen ${⊢}\forall {z}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)\phantom{\rule{.4em}{0ex}}\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\exists {b}\in {B}\phantom{\rule{.4em}{0ex}}{z}={a}{F}{b}$
61 foov ${⊢}{F}:{A}×{B}\underset{onto}{⟶}\underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)↔\left({F}:{A}×{B}⟶\underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)\wedge \forall {z}\in \underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)\phantom{\rule{.4em}{0ex}}\exists {a}\in {A}\phantom{\rule{.4em}{0ex}}\exists {b}\in {B}\phantom{\rule{.4em}{0ex}}{z}={a}{F}{b}\right)$
62 6 60 61 mpbir2an ${⊢}{F}:{A}×{B}\underset{onto}{⟶}\underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)$
63 df-f1o ${⊢}{F}:{A}×{B}\underset{1-1 onto}{⟶}\underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)↔\left({F}:{A}×{B}\underset{1-1}{⟶}\underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)\wedge {F}:{A}×{B}\underset{onto}{⟶}\underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)\right)$
64 48 62 63 mpbir2an ${⊢}{F}:{A}×{B}\underset{1-1 onto}{⟶}\underset{{k}\in {2}_{𝑜}}{⨉}if\left({k}=\varnothing ,{A},{B}\right)$