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 BV1stA×B:A×B1-1 ontoA

Proof

Step Hyp Ref Expression
1 snnzg BVB
2 fo1stres B1stA×B:A×BontoA
3 1 2 syl BV1stA×B:A×BontoA
4 moeq *xx=yB
5 4 moani *xyAx=yB
6 vex yV
7 6 brresi x1stA×ByxA×Bx1sty
8 fo1st 1st:VontoV
9 fofn 1st:VontoV1stFnV
10 8 9 ax-mp 1stFnV
11 vex xV
12 fnbrfvb 1stFnVxV1stx=yx1sty
13 10 11 12 mp2an 1stx=yx1sty
14 13 anbi2i xA×B1stx=yxA×Bx1sty
15 elxp7 xA×BxV×V1stxA2ndxB
16 eleq1 1stx=y1stxAyA
17 16 biimpac 1stxA1stx=yyA
18 17 adantlr 1stxA2ndxB1stx=yyA
19 18 adantll xV×V1stxA2ndxB1stx=yyA
20 elsni 2ndxB2ndx=B
21 eqopi xV×V1stx=y2ndx=Bx=yB
22 21 anass1rs xV×V2ndx=B1stx=yx=yB
23 20 22 sylanl2 xV×V2ndxB1stx=yx=yB
24 23 adantlrl xV×V1stxA2ndxB1stx=yx=yB
25 19 24 jca xV×V1stxA2ndxB1stx=yyAx=yB
26 15 25 sylanb xA×B1stx=yyAx=yB
27 26 adantl BVxA×B1stx=yyAx=yB
28 simprr BVyAx=yBx=yB
29 simprl BVyAx=yByA
30 snidg BVBB
31 30 adantr BVyAx=yBBB
32 29 31 opelxpd BVyAx=yByBA×B
33 28 32 eqeltrd BVyAx=yBxA×B
34 28 fveq2d BVyAx=yB1stx=1styB
35 simpl BVyAx=yBBV
36 op1stg yABV1styB=y
37 29 35 36 syl2anc BVyAx=yB1styB=y
38 34 37 eqtrd BVyAx=yB1stx=y
39 33 38 jca BVyAx=yBxA×B1stx=y
40 27 39 impbida BVxA×B1stx=yyAx=yB
41 14 40 bitr3id BVxA×Bx1styyAx=yB
42 7 41 bitrid BVx1stA×ByyAx=yB
43 42 mobidv BV*xx1stA×By*xyAx=yB
44 5 43 mpbiri BV*xx1stA×By
45 44 alrimiv BVy*xx1stA×By
46 funcnv2 Fun1stA×B-1y*xx1stA×By
47 45 46 sylibr BVFun1stA×B-1
48 dff1o3 1stA×B:A×B1-1 ontoA1stA×B:A×BontoAFun1stA×B-1
49 3 47 48 sylanbrc BV1stA×B:A×B1-1 ontoA