Metamath Proof Explorer


Theorem projf1o

Description: A biijection from a set to a projection in a two dimensional space. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses projf1o.1 φ A V
projf1o.2 F = x B A x
Assertion projf1o φ F : B 1-1 onto A × B

Proof

Step Hyp Ref Expression
1 projf1o.1 φ A V
2 projf1o.2 F = x B A x
3 snidg A V A A
4 1 3 syl φ A A
5 4 adantr φ y B A A
6 simpr φ y B y B
7 5 6 opelxpd φ y B A y A × B
8 opeq2 x = y A x = A y
9 8 cbvmptv x B A x = y B A y
10 2 9 eqtri F = y B A y
11 7 10 fmptd φ F : B A × B
12 simpl1 φ y B z B F y = F z φ
13 2 8 6 7 fvmptd3 φ y B F y = A y
14 13 eqcomd φ y B A y = F y
15 14 3adant3 φ y B z B A y = F y
16 15 adantr φ y B z B F y = F z A y = F y
17 simpr φ y B z B F y = F z F y = F z
18 opeq2 y = z A y = A z
19 simpr φ z B z B
20 opex A z V
21 20 a1i φ z B A z V
22 10 18 19 21 fvmptd3 φ z B F z = A z
23 22 3adant2 φ y B z B F z = A z
24 23 adantr φ y B z B F y = F z F z = A z
25 16 17 24 3eqtrd φ y B z B F y = F z A y = A z
26 vex z V
27 26 a1i φ z V
28 opthg2 A V z V A y = A z A = A y = z
29 1 27 28 syl2anc φ A y = A z A = A y = z
30 29 simplbda φ A y = A z y = z
31 12 25 30 syl2anc φ y B z B F y = F z y = z
32 31 ex φ y B z B F y = F z y = z
33 32 3expb φ y B z B F y = F z y = z
34 33 ralrimivva φ y B z B F y = F z y = z
35 dff13 F : B 1-1 A × B F : B A × B y B z B F y = F z y = z
36 11 34 35 sylanbrc φ F : B 1-1 A × B
37 elsnxp A V z A × B y B z = A y
38 1 37 syl φ z A × B y B z = A y
39 38 biimpa φ z A × B y B z = A y
40 13 adantr φ y B z = A y F y = A y
41 id z = A y z = A y
42 41 eqcomd z = A y A y = z
43 42 adantl φ y B z = A y A y = z
44 40 43 eqtr2d φ y B z = A y z = F y
45 44 ex φ y B z = A y z = F y
46 45 adantlr φ z A × B y B z = A y z = F y
47 46 reximdva φ z A × B y B z = A y y B z = F y
48 39 47 mpd φ z A × B y B z = F y
49 48 ralrimiva φ z A × B y B z = F y
50 dffo3 F : B onto A × B F : B A × B z A × B y B z = F y
51 11 49 50 sylanbrc φ F : B onto A × B
52 df-f1o F : B 1-1 onto A × B F : B 1-1 A × B F : B onto A × B
53 36 51 52 sylanbrc φ F : B 1-1 onto A × B