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 
|- ( ph -> A e. V )
projf1o.2 
|- F = ( x e. B |-> <. A , x >. )
Assertion projf1o 
|- ( ph -> F : B -1-1-onto-> ( { A } X. B ) )

Proof

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