Metamath Proof Explorer


Theorem 1stfcl

Description: The first projection functor is a functor onto the left argument. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses 1stfcl.t T = C × c D
1stfcl.c φ C Cat
1stfcl.d φ D Cat
1stfcl.p P = C 1 st F D
Assertion 1stfcl φ P T Func C

Proof

Step Hyp Ref Expression
1 1stfcl.t T = C × c D
2 1stfcl.c φ C Cat
3 1stfcl.d φ D Cat
4 1stfcl.p P = C 1 st F D
5 eqid Base C = Base C
6 eqid Base D = Base D
7 1 5 6 xpcbas Base C × Base D = Base T
8 eqid Hom T = Hom T
9 1 7 8 2 3 4 1stfval φ P = 1 st Base C × Base D x Base C × Base D , y Base C × Base D 1 st x Hom T y
10 fo1st 1 st : V onto V
11 fofun 1 st : V onto V Fun 1 st
12 10 11 ax-mp Fun 1 st
13 fvex Base C V
14 fvex Base D V
15 13 14 xpex Base C × Base D V
16 resfunexg Fun 1 st Base C × Base D V 1 st Base C × Base D V
17 12 15 16 mp2an 1 st Base C × Base D V
18 15 15 mpoex x Base C × Base D , y Base C × Base D 1 st x Hom T y V
19 17 18 op2ndd P = 1 st Base C × Base D x Base C × Base D , y Base C × Base D 1 st x Hom T y 2 nd P = x Base C × Base D , y Base C × Base D 1 st x Hom T y
20 9 19 syl φ 2 nd P = x Base C × Base D , y Base C × Base D 1 st x Hom T y
21 20 opeq2d φ 1 st Base C × Base D 2 nd P = 1 st Base C × Base D x Base C × Base D , y Base C × Base D 1 st x Hom T y
22 9 21 eqtr4d φ P = 1 st Base C × Base D 2 nd P
23 eqid Hom C = Hom C
24 eqid Id T = Id T
25 eqid Id C = Id C
26 eqid comp T = comp T
27 eqid comp C = comp C
28 1 2 3 xpccat φ T Cat
29 f1stres 1 st Base C × Base D : Base C × Base D Base C
30 29 a1i φ 1 st Base C × Base D : Base C × Base D Base C
31 eqid x Base C × Base D , y Base C × Base D 1 st x Hom T y = x Base C × Base D , y Base C × Base D 1 st x Hom T y
32 ovex x Hom T y V
33 resfunexg Fun 1 st x Hom T y V 1 st x Hom T y V
34 12 32 33 mp2an 1 st x Hom T y V
35 31 34 fnmpoi x Base C × Base D , y Base C × Base D 1 st x Hom T y Fn Base C × Base D × Base C × Base D
36 20 fneq1d φ 2 nd P Fn Base C × Base D × Base C × Base D x Base C × Base D , y Base C × Base D 1 st x Hom T y Fn Base C × Base D × Base C × Base D
37 35 36 mpbiri φ 2 nd P Fn Base C × Base D × Base C × Base D
38 f1stres 1 st 1 st x Hom C 1 st y × 2 nd x Hom D 2 nd y : 1 st x Hom C 1 st y × 2 nd x Hom D 2 nd y 1 st x Hom C 1 st y
39 2 adantr φ x Base C × Base D y Base C × Base D C Cat
40 3 adantr φ x Base C × Base D y Base C × Base D D Cat
41 simprl φ x Base C × Base D y Base C × Base D x Base C × Base D
42 simprr φ x Base C × Base D y Base C × Base D y Base C × Base D
43 1 7 8 39 40 4 41 42 1stf2 φ x Base C × Base D y Base C × Base D x 2 nd P y = 1 st x Hom T y
44 eqid Hom D = Hom D
45 1 7 23 44 8 41 42 xpchom φ x Base C × Base D y Base C × Base D x Hom T y = 1 st x Hom C 1 st y × 2 nd x Hom D 2 nd y
46 45 reseq2d φ x Base C × Base D y Base C × Base D 1 st x Hom T y = 1 st 1 st x Hom C 1 st y × 2 nd x Hom D 2 nd y
47 43 46 eqtrd φ x Base C × Base D y Base C × Base D x 2 nd P y = 1 st 1 st x Hom C 1 st y × 2 nd x Hom D 2 nd y
48 47 feq1d φ x Base C × Base D y Base C × Base D x 2 nd P y : 1 st x Hom C 1 st y × 2 nd x Hom D 2 nd y 1 st x Hom C 1 st y 1 st 1 st x Hom C 1 st y × 2 nd x Hom D 2 nd y : 1 st x Hom C 1 st y × 2 nd x Hom D 2 nd y 1 st x Hom C 1 st y
49 38 48 mpbiri φ x Base C × Base D y Base C × Base D x 2 nd P y : 1 st x Hom C 1 st y × 2 nd x Hom D 2 nd y 1 st x Hom C 1 st y
50 fvres x Base C × Base D 1 st Base C × Base D x = 1 st x
51 50 ad2antrl φ x Base C × Base D y Base C × Base D 1 st Base C × Base D x = 1 st x
52 fvres y Base C × Base D 1 st Base C × Base D y = 1 st y
53 52 ad2antll φ x Base C × Base D y Base C × Base D 1 st Base C × Base D y = 1 st y
54 51 53 oveq12d φ x Base C × Base D y Base C × Base D 1 st Base C × Base D x Hom C 1 st Base C × Base D y = 1 st x Hom C 1 st y
55 45 54 feq23d φ x Base C × Base D y Base C × Base D x 2 nd P y : x Hom T y 1 st Base C × Base D x Hom C 1 st Base C × Base D y x 2 nd P y : 1 st x Hom C 1 st y × 2 nd x Hom D 2 nd y 1 st x Hom C 1 st y
56 49 55 mpbird φ x Base C × Base D y Base C × Base D x 2 nd P y : x Hom T y 1 st Base C × Base D x Hom C 1 st Base C × Base D y
57 28 adantr φ x Base C × Base D T Cat
58 simpr φ x Base C × Base D x Base C × Base D
59 7 8 24 57 58 catidcl φ x Base C × Base D Id T x x Hom T x
60 59 fvresd φ x Base C × Base D 1 st x Hom T x Id T x = 1 st Id T x
61 1st2nd2 x Base C × Base D x = 1 st x 2 nd x
62 61 adantl φ x Base C × Base D x = 1 st x 2 nd x
63 62 fveq2d φ x Base C × Base D Id T x = Id T 1 st x 2 nd x
64 2 adantr φ x Base C × Base D C Cat
65 3 adantr φ x Base C × Base D D Cat
66 eqid Id D = Id D
67 xp1st x Base C × Base D 1 st x Base C
68 67 adantl φ x Base C × Base D 1 st x Base C
69 xp2nd x Base C × Base D 2 nd x Base D
70 69 adantl φ x Base C × Base D 2 nd x Base D
71 1 64 65 5 6 25 66 24 68 70 xpcid φ x Base C × Base D Id T 1 st x 2 nd x = Id C 1 st x Id D 2 nd x
72 63 71 eqtrd φ x Base C × Base D Id T x = Id C 1 st x Id D 2 nd x
73 fvex Id C 1 st x V
74 fvex Id D 2 nd x V
75 73 74 op1std Id T x = Id C 1 st x Id D 2 nd x 1 st Id T x = Id C 1 st x
76 72 75 syl φ x Base C × Base D 1 st Id T x = Id C 1 st x
77 60 76 eqtrd φ x Base C × Base D 1 st x Hom T x Id T x = Id C 1 st x
78 1 7 8 64 65 4 58 58 1stf2 φ x Base C × Base D x 2 nd P x = 1 st x Hom T x
79 78 fveq1d φ x Base C × Base D x 2 nd P x Id T x = 1 st x Hom T x Id T x
80 50 adantl φ x Base C × Base D 1 st Base C × Base D x = 1 st x
81 80 fveq2d φ x Base C × Base D Id C 1 st Base C × Base D x = Id C 1 st x
82 77 79 81 3eqtr4d φ x Base C × Base D x 2 nd P x Id T x = Id C 1 st Base C × Base D x
83 28 3ad2ant1 φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z T Cat
84 simp21 φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z x Base C × Base D
85 simp22 φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z y Base C × Base D
86 simp23 φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z z Base C × Base D
87 simp3l φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z f x Hom T y
88 simp3r φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z g y Hom T z
89 7 8 26 83 84 85 86 87 88 catcocl φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z g x y comp T z f x Hom T z
90 89 fvresd φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z 1 st x Hom T z g x y comp T z f = 1 st g x y comp T z f
91 1 7 8 26 84 85 86 87 88 27 xpcco1st φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z 1 st g x y comp T z f = 1 st g 1 st x 1 st y comp C 1 st z 1 st f
92 90 91 eqtrd φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z 1 st x Hom T z g x y comp T z f = 1 st g 1 st x 1 st y comp C 1 st z 1 st f
93 2 3ad2ant1 φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z C Cat
94 3 3ad2ant1 φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z D Cat
95 1 7 8 93 94 4 84 86 1stf2 φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z x 2 nd P z = 1 st x Hom T z
96 95 fveq1d φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z x 2 nd P z g x y comp T z f = 1 st x Hom T z g x y comp T z f
97 84 fvresd φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z 1 st Base C × Base D x = 1 st x
98 85 fvresd φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z 1 st Base C × Base D y = 1 st y
99 97 98 opeq12d φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z 1 st Base C × Base D x 1 st Base C × Base D y = 1 st x 1 st y
100 86 fvresd φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z 1 st Base C × Base D z = 1 st z
101 99 100 oveq12d φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z 1 st Base C × Base D x 1 st Base C × Base D y comp C 1 st Base C × Base D z = 1 st x 1 st y comp C 1 st z
102 1 7 8 93 94 4 85 86 1stf2 φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z y 2 nd P z = 1 st y Hom T z
103 102 fveq1d φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z y 2 nd P z g = 1 st y Hom T z g
104 88 fvresd φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z 1 st y Hom T z g = 1 st g
105 103 104 eqtrd φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z y 2 nd P z g = 1 st g
106 1 7 8 93 94 4 84 85 1stf2 φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z x 2 nd P y = 1 st x Hom T y
107 106 fveq1d φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z x 2 nd P y f = 1 st x Hom T y f
108 87 fvresd φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z 1 st x Hom T y f = 1 st f
109 107 108 eqtrd φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z x 2 nd P y f = 1 st f
110 101 105 109 oveq123d φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z y 2 nd P z g 1 st Base C × Base D x 1 st Base C × Base D y comp C 1 st Base C × Base D z x 2 nd P y f = 1 st g 1 st x 1 st y comp C 1 st z 1 st f
111 92 96 110 3eqtr4d φ x Base C × Base D y Base C × Base D z Base C × Base D f x Hom T y g y Hom T z x 2 nd P z g x y comp T z f = y 2 nd P z g 1 st Base C × Base D x 1 st Base C × Base D y comp C 1 st Base C × Base D z x 2 nd P y f
112 7 5 8 23 24 25 26 27 28 2 30 37 56 82 111 isfuncd φ 1 st Base C × Base D T Func C 2 nd P
113 df-br 1 st Base C × Base D T Func C 2 nd P 1 st Base C × Base D 2 nd P T Func C
114 112 113 sylib φ 1 st Base C × Base D 2 nd P T Func C
115 22 114 eqeltrd φ P T Func C