Metamath Proof Explorer


Theorem 1stconst

Description: The mapping of a restriction of the 1st function to a constant function. (Contributed by NM, 14-Dec-2008) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion 1stconst B V 1 st A × B : A × B 1-1 onto A

Proof

Step Hyp Ref Expression
1 snnzg B V B
2 fo1stres B 1 st A × B : A × B onto A
3 1 2 syl B V 1 st A × B : A × B onto A
4 moeq * x x = y B
5 4 moani * x y A x = y B
6 vex y V
7 6 brresi x 1 st A × B y x A × B x 1 st y
8 fo1st 1 st : V onto V
9 fofn 1 st : V onto V 1 st Fn V
10 8 9 ax-mp 1 st Fn V
11 vex x V
12 fnbrfvb 1 st Fn V x V 1 st x = y x 1 st y
13 10 11 12 mp2an 1 st x = y x 1 st y
14 13 anbi2i x A × B 1 st x = y x A × B x 1 st y
15 elxp7 x A × B x V × V 1 st x A 2 nd x B
16 eleq1 1 st x = y 1 st x A y A
17 16 biimpac 1 st x A 1 st x = y y A
18 17 adantlr 1 st x A 2 nd x B 1 st x = y y A
19 18 adantll x V × V 1 st x A 2 nd x B 1 st x = y y A
20 elsni 2 nd x B 2 nd x = B
21 eqopi x V × V 1 st x = y 2 nd x = B x = y B
22 21 anass1rs x V × V 2 nd x = B 1 st x = y x = y B
23 20 22 sylanl2 x V × V 2 nd x B 1 st x = y x = y B
24 23 adantlrl x V × V 1 st x A 2 nd x B 1 st x = y x = y B
25 19 24 jca x V × V 1 st x A 2 nd x B 1 st x = y y A x = y B
26 15 25 sylanb x A × B 1 st x = y y A x = y B
27 26 adantl B V x A × B 1 st x = y y A x = y B
28 simprr B V y A x = y B x = y B
29 simprl B V y A x = y B y A
30 snidg B V B B
31 30 adantr B V y A x = y B B B
32 29 31 opelxpd B V y A x = y B y B A × B
33 28 32 eqeltrd B V y A x = y B x A × B
34 28 fveq2d B V y A x = y B 1 st x = 1 st y B
35 simpl B V y A x = y B B V
36 op1stg y A B V 1 st y B = y
37 29 35 36 syl2anc B V y A x = y B 1 st y B = y
38 34 37 eqtrd B V y A x = y B 1 st x = y
39 33 38 jca B V y A x = y B x A × B 1 st x = y
40 27 39 impbida B V x A × B 1 st x = y y A x = y B
41 14 40 bitr3id B V x A × B x 1 st y y A x = y B
42 7 41 syl5bb B V x 1 st A × B y y A x = y B
43 42 mobidv B V * x x 1 st A × B y * x y A x = y B
44 5 43 mpbiri B V * x x 1 st A × B y
45 44 alrimiv B V y * x x 1 st A × B y
46 funcnv2 Fun 1 st A × B -1 y * x x 1 st A × B y
47 45 46 sylibr B V Fun 1 st A × B -1
48 dff1o3 1 st A × B : A × B 1-1 onto A 1 st A × B : A × B onto A Fun 1 st A × B -1
49 3 47 48 sylanbrc B V 1 st A × B : A × B 1-1 onto A