Metamath Proof Explorer


Theorem 2ndconst

Description: The mapping of a restriction of the 2nd function to a converse constant function. (Contributed by NM, 27-Mar-2008) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion 2ndconst AV2ndA×B:A×B1-1 ontoB

Proof

Step Hyp Ref Expression
1 snnzg AVA
2 fo2ndres A2ndA×B:A×BontoB
3 1 2 syl AV2ndA×B:A×BontoB
4 moeq *xx=Ay
5 4 moani *xyBx=Ay
6 vex yV
7 6 brresi x2ndA×ByxA×Bx2ndy
8 fo2nd 2nd:VontoV
9 fofn 2nd:VontoV2ndFnV
10 8 9 ax-mp 2ndFnV
11 vex xV
12 fnbrfvb 2ndFnVxV2ndx=yx2ndy
13 10 11 12 mp2an 2ndx=yx2ndy
14 13 anbi2i xA×B2ndx=yxA×Bx2ndy
15 elxp7 xA×BxV×V1stxA2ndxB
16 eleq1 2ndx=y2ndxByB
17 16 biimpac 2ndxB2ndx=yyB
18 17 adantll 1stxA2ndxB2ndx=yyB
19 18 adantll xV×V1stxA2ndxB2ndx=yyB
20 elsni 1stxA1stx=A
21 eqopi xV×V1stx=A2ndx=yx=Ay
22 21 anassrs xV×V1stx=A2ndx=yx=Ay
23 20 22 sylanl2 xV×V1stxA2ndx=yx=Ay
24 23 adantlrr xV×V1stxA2ndxB2ndx=yx=Ay
25 19 24 jca xV×V1stxA2ndxB2ndx=yyBx=Ay
26 15 25 sylanb xA×B2ndx=yyBx=Ay
27 26 adantl AVxA×B2ndx=yyBx=Ay
28 simprr AVyBx=Ayx=Ay
29 snidg AVAA
30 29 adantr AVyBx=AyAA
31 simprl AVyBx=AyyB
32 30 31 opelxpd AVyBx=AyAyA×B
33 28 32 eqeltrd AVyBx=AyxA×B
34 fveq2 x=Ay2ndx=2ndAy
35 op2ndg AVyV2ndAy=y
36 35 elvd AV2ndAy=y
37 34 36 sylan9eqr AVx=Ay2ndx=y
38 37 adantrl AVyBx=Ay2ndx=y
39 33 38 jca AVyBx=AyxA×B2ndx=y
40 27 39 impbida AVxA×B2ndx=yyBx=Ay
41 14 40 bitr3id AVxA×Bx2ndyyBx=Ay
42 7 41 bitrid AVx2ndA×ByyBx=Ay
43 42 mobidv AV*xx2ndA×By*xyBx=Ay
44 5 43 mpbiri AV*xx2ndA×By
45 44 alrimiv AVy*xx2ndA×By
46 funcnv2 Fun2ndA×B-1y*xx2ndA×By
47 45 46 sylibr AVFun2ndA×B-1
48 dff1o3 2ndA×B:A×B1-1 ontoB2ndA×B:A×BontoBFun2ndA×B-1
49 3 47 48 sylanbrc AV2ndA×B:A×B1-1 ontoB