Metamath Proof Explorer


Theorem prf2nd

Description: Cancellation of pairing with second projection. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses prf1st.p P = F ⟨,⟩ F G
prf1st.c φ F C Func D
prf1st.d φ G C Func E
Assertion prf2nd φ D 2 nd F E func P = G

Proof

Step Hyp Ref Expression
1 prf1st.p P = F ⟨,⟩ F G
2 prf1st.c φ F C Func D
3 prf1st.d φ G C Func E
4 eqid D × c E = D × c E
5 eqid Base D = Base D
6 eqid Base E = Base E
7 4 5 6 xpcbas Base D × Base E = Base D × c E
8 eqid Hom D × c E = Hom D × c E
9 funcrcl F C Func D C Cat D Cat
10 2 9 syl φ C Cat D Cat
11 10 simprd φ D Cat
12 11 adantr φ x Base C D Cat
13 funcrcl G C Func E C Cat E Cat
14 3 13 syl φ C Cat E Cat
15 14 simprd φ E Cat
16 15 adantr φ x Base C E Cat
17 eqid D 2 nd F E = D 2 nd F E
18 eqid Base C = Base C
19 relfunc Rel C Func D
20 1st2ndbr Rel C Func D F C Func D 1 st F C Func D 2 nd F
21 19 2 20 sylancr φ 1 st F C Func D 2 nd F
22 18 5 21 funcf1 φ 1 st F : Base C Base D
23 22 ffvelrnda φ x Base C 1 st F x Base D
24 relfunc Rel C Func E
25 1st2ndbr Rel C Func E G C Func E 1 st G C Func E 2 nd G
26 24 3 25 sylancr φ 1 st G C Func E 2 nd G
27 18 6 26 funcf1 φ 1 st G : Base C Base E
28 27 ffvelrnda φ x Base C 1 st G x Base E
29 23 28 opelxpd φ x Base C 1 st F x 1 st G x Base D × Base E
30 4 7 8 12 16 17 29 2ndf1 φ x Base C 1 st D 2 nd F E 1 st F x 1 st G x = 2 nd 1 st F x 1 st G x
31 fvex 1 st F x V
32 fvex 1 st G x V
33 31 32 op2nd 2 nd 1 st F x 1 st G x = 1 st G x
34 30 33 eqtrdi φ x Base C 1 st D 2 nd F E 1 st F x 1 st G x = 1 st G x
35 34 mpteq2dva φ x Base C 1 st D 2 nd F E 1 st F x 1 st G x = x Base C 1 st G x
36 eqid Hom C = Hom C
37 1 18 36 2 3 prfval φ P = x Base C 1 st F x 1 st G x x Base C , y Base C h x Hom C y x 2 nd F y h x 2 nd G y h
38 fvex Base C V
39 38 mptex x Base C 1 st F x 1 st G x V
40 38 38 mpoex x Base C , y Base C h x Hom C y x 2 nd F y h x 2 nd G y h V
41 39 40 op1std P = x Base C 1 st F x 1 st G x x Base C , y Base C h x Hom C y x 2 nd F y h x 2 nd G y h 1 st P = x Base C 1 st F x 1 st G x
42 37 41 syl φ 1 st P = x Base C 1 st F x 1 st G x
43 relfunc Rel D × c E Func E
44 4 11 15 17 2ndfcl φ D 2 nd F E D × c E Func E
45 1st2ndbr Rel D × c E Func E D 2 nd F E D × c E Func E 1 st D 2 nd F E D × c E Func E 2 nd D 2 nd F E
46 43 44 45 sylancr φ 1 st D 2 nd F E D × c E Func E 2 nd D 2 nd F E
47 7 6 46 funcf1 φ 1 st D 2 nd F E : Base D × Base E Base E
48 47 feqmptd φ 1 st D 2 nd F E = u Base D × Base E 1 st D 2 nd F E u
49 fveq2 u = 1 st F x 1 st G x 1 st D 2 nd F E u = 1 st D 2 nd F E 1 st F x 1 st G x
50 29 42 48 49 fmptco φ 1 st D 2 nd F E 1 st P = x Base C 1 st D 2 nd F E 1 st F x 1 st G x
51 27 feqmptd φ 1 st G = x Base C 1 st G x
52 35 50 51 3eqtr4d φ 1 st D 2 nd F E 1 st P = 1 st G
53 11 ad2antrr φ x Base C y Base C f x Hom C y D Cat
54 15 ad2antrr φ x Base C y Base C f x Hom C y E Cat
55 relfunc Rel C Func D × c E
56 1 4 2 3 prfcl φ P C Func D × c E
57 1st2ndbr Rel C Func D × c E P C Func D × c E 1 st P C Func D × c E 2 nd P
58 55 56 57 sylancr φ 1 st P C Func D × c E 2 nd P
59 18 7 58 funcf1 φ 1 st P : Base C Base D × Base E
60 59 ffvelrnda φ x Base C 1 st P x Base D × Base E
61 60 adantrr φ x Base C y Base C 1 st P x Base D × Base E
62 61 adantr φ x Base C y Base C f x Hom C y 1 st P x Base D × Base E
63 59 ffvelrnda φ y Base C 1 st P y Base D × Base E
64 63 adantrl φ x Base C y Base C 1 st P y Base D × Base E
65 64 adantr φ x Base C y Base C f x Hom C y 1 st P y Base D × Base E
66 4 7 8 53 54 17 62 65 2ndf2 φ x Base C y Base C f x Hom C y 1 st P x 2 nd D 2 nd F E 1 st P y = 2 nd 1 st P x Hom D × c E 1 st P y
67 66 fveq1d φ x Base C y Base C f x Hom C y 1 st P x 2 nd D 2 nd F E 1 st P y x 2 nd P y f = 2 nd 1 st P x Hom D × c E 1 st P y x 2 nd P y f
68 58 adantr φ x Base C y Base C 1 st P C Func D × c E 2 nd P
69 simprl φ x Base C y Base C x Base C
70 simprr φ x Base C y Base C y Base C
71 18 36 8 68 69 70 funcf2 φ x Base C y Base C x 2 nd P y : x Hom C y 1 st P x Hom D × c E 1 st P y
72 71 ffvelrnda φ x Base C y Base C f x Hom C y x 2 nd P y f 1 st P x Hom D × c E 1 st P y
73 72 fvresd φ x Base C y Base C f x Hom C y 2 nd 1 st P x Hom D × c E 1 st P y x 2 nd P y f = 2 nd x 2 nd P y f
74 2 ad2antrr φ x Base C y Base C f x Hom C y F C Func D
75 3 ad2antrr φ x Base C y Base C f x Hom C y G C Func E
76 69 adantr φ x Base C y Base C f x Hom C y x Base C
77 70 adantr φ x Base C y Base C f x Hom C y y Base C
78 simpr φ x Base C y Base C f x Hom C y f x Hom C y
79 1 18 36 74 75 76 77 78 prf2 φ x Base C y Base C f x Hom C y x 2 nd P y f = x 2 nd F y f x 2 nd G y f
80 79 fveq2d φ x Base C y Base C f x Hom C y 2 nd x 2 nd P y f = 2 nd x 2 nd F y f x 2 nd G y f
81 fvex x 2 nd F y f V
82 fvex x 2 nd G y f V
83 81 82 op2nd 2 nd x 2 nd F y f x 2 nd G y f = x 2 nd G y f
84 80 83 eqtrdi φ x Base C y Base C f x Hom C y 2 nd x 2 nd P y f = x 2 nd G y f
85 67 73 84 3eqtrd φ x Base C y Base C f x Hom C y 1 st P x 2 nd D 2 nd F E 1 st P y x 2 nd P y f = x 2 nd G y f
86 85 mpteq2dva φ x Base C y Base C f x Hom C y 1 st P x 2 nd D 2 nd F E 1 st P y x 2 nd P y f = f x Hom C y x 2 nd G y f
87 eqid Hom E = Hom E
88 46 adantr φ x Base C y Base C 1 st D 2 nd F E D × c E Func E 2 nd D 2 nd F E
89 7 8 87 88 61 64 funcf2 φ x Base C y Base C 1 st P x 2 nd D 2 nd F E 1 st P y : 1 st P x Hom D × c E 1 st P y 1 st D 2 nd F E 1 st P x Hom E 1 st D 2 nd F E 1 st P y
90 fcompt 1 st P x 2 nd D 2 nd F E 1 st P y : 1 st P x Hom D × c E 1 st P y 1 st D 2 nd F E 1 st P x Hom E 1 st D 2 nd F E 1 st P y x 2 nd P y : x Hom C y 1 st P x Hom D × c E 1 st P y 1 st P x 2 nd D 2 nd F E 1 st P y x 2 nd P y = f x Hom C y 1 st P x 2 nd D 2 nd F E 1 st P y x 2 nd P y f
91 89 71 90 syl2anc φ x Base C y Base C 1 st P x 2 nd D 2 nd F E 1 st P y x 2 nd P y = f x Hom C y 1 st P x 2 nd D 2 nd F E 1 st P y x 2 nd P y f
92 26 adantr φ x Base C y Base C 1 st G C Func E 2 nd G
93 18 36 87 92 69 70 funcf2 φ x Base C y Base C x 2 nd G y : x Hom C y 1 st G x Hom E 1 st G y
94 93 feqmptd φ x Base C y Base C x 2 nd G y = f x Hom C y x 2 nd G y f
95 86 91 94 3eqtr4d φ x Base C y Base C 1 st P x 2 nd D 2 nd F E 1 st P y x 2 nd P y = x 2 nd G y
96 95 3impb φ x Base C y Base C 1 st P x 2 nd D 2 nd F E 1 st P y x 2 nd P y = x 2 nd G y
97 96 mpoeq3dva φ x Base C , y Base C 1 st P x 2 nd D 2 nd F E 1 st P y x 2 nd P y = x Base C , y Base C x 2 nd G y
98 18 26 funcfn2 φ 2 nd G Fn Base C × Base C
99 fnov 2 nd G Fn Base C × Base C 2 nd G = x Base C , y Base C x 2 nd G y
100 98 99 sylib φ 2 nd G = x Base C , y Base C x 2 nd G y
101 97 100 eqtr4d φ x Base C , y Base C 1 st P x 2 nd D 2 nd F E 1 st P y x 2 nd P y = 2 nd G
102 52 101 opeq12d φ 1 st D 2 nd F E 1 st P x Base C , y Base C 1 st P x 2 nd D 2 nd F E 1 st P y x 2 nd P y = 1 st G 2 nd G
103 18 56 44 cofuval φ D 2 nd F E func P = 1 st D 2 nd F E 1 st P x Base C , y Base C 1 st P x 2 nd D 2 nd F E 1 st P y x 2 nd P y
104 1st2nd Rel C Func E G C Func E G = 1 st G 2 nd G
105 24 3 104 sylancr φ G = 1 st G 2 nd G
106 102 103 105 3eqtr4d φ D 2 nd F E func P = G