Metamath Proof Explorer


Theorem isfull

Description: Value of the set of full functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses isfull.b B = Base C
isfull.j J = Hom D
Assertion isfull F C Full D G F C Func D G x B y B ran x G y = F x J F y

Proof

Step Hyp Ref Expression
1 isfull.b B = Base C
2 isfull.j J = Hom D
3 fullfunc C Full D C Func D
4 3 ssbri F C Full D G F C Func D G
5 df-br F C Func D G F G C Func D
6 funcrcl F G C Func D C Cat D Cat
7 5 6 sylbi F C Func D G C Cat D Cat
8 oveq12 c = C d = D c Func d = C Func D
9 8 breqd c = C d = D f c Func d g f C Func D g
10 simpl c = C d = D c = C
11 10 fveq2d c = C d = D Base c = Base C
12 11 1 eqtr4di c = C d = D Base c = B
13 simpr c = C d = D d = D
14 13 fveq2d c = C d = D Hom d = Hom D
15 14 2 eqtr4di c = C d = D Hom d = J
16 15 oveqd c = C d = D f x Hom d f y = f x J f y
17 16 eqeq2d c = C d = D ran x g y = f x Hom d f y ran x g y = f x J f y
18 12 17 raleqbidv c = C d = D y Base c ran x g y = f x Hom d f y y B ran x g y = f x J f y
19 12 18 raleqbidv c = C d = D x Base c y Base c ran x g y = f x Hom d f y x B y B ran x g y = f x J f y
20 9 19 anbi12d c = C d = D f c Func d g x Base c y Base c ran x g y = f x Hom d f y f C Func D g x B y B ran x g y = f x J f y
21 20 opabbidv c = C d = D f g | f c Func d g x Base c y Base c ran x g y = f x Hom d f y = f g | f C Func D g x B y B ran x g y = f x J f y
22 df-full Full = c Cat , d Cat f g | f c Func d g x Base c y Base c ran x g y = f x Hom d f y
23 ovex C Func D V
24 simpl f C Func D g x B y B ran x g y = f x J f y f C Func D g
25 24 ssopab2i f g | f C Func D g x B y B ran x g y = f x J f y f g | f C Func D g
26 opabss f g | f C Func D g C Func D
27 25 26 sstri f g | f C Func D g x B y B ran x g y = f x J f y C Func D
28 23 27 ssexi f g | f C Func D g x B y B ran x g y = f x J f y V
29 21 22 28 ovmpoa C Cat D Cat C Full D = f g | f C Func D g x B y B ran x g y = f x J f y
30 7 29 syl F C Func D G C Full D = f g | f C Func D g x B y B ran x g y = f x J f y
31 30 breqd F C Func D G F C Full D G F f g | f C Func D g x B y B ran x g y = f x J f y G
32 relfunc Rel C Func D
33 32 brrelex12i F C Func D G F V G V
34 breq12 f = F g = G f C Func D g F C Func D G
35 simpr f = F g = G g = G
36 35 oveqd f = F g = G x g y = x G y
37 36 rneqd f = F g = G ran x g y = ran x G y
38 simpl f = F g = G f = F
39 38 fveq1d f = F g = G f x = F x
40 38 fveq1d f = F g = G f y = F y
41 39 40 oveq12d f = F g = G f x J f y = F x J F y
42 37 41 eqeq12d f = F g = G ran x g y = f x J f y ran x G y = F x J F y
43 42 2ralbidv f = F g = G x B y B ran x g y = f x J f y x B y B ran x G y = F x J F y
44 34 43 anbi12d f = F g = G f C Func D g x B y B ran x g y = f x J f y F C Func D G x B y B ran x G y = F x J F y
45 eqid f g | f C Func D g x B y B ran x g y = f x J f y = f g | f C Func D g x B y B ran x g y = f x J f y
46 44 45 brabga F V G V F f g | f C Func D g x B y B ran x g y = f x J f y G F C Func D G x B y B ran x G y = F x J F y
47 33 46 syl F C Func D G F f g | f C Func D g x B y B ran x g y = f x J f y G F C Func D G x B y B ran x G y = F x J F y
48 31 47 bitrd F C Func D G F C Full D G F C Func D G x B y B ran x G y = F x J F y
49 48 bianabs F C Func D G F C Full D G x B y B ran x G y = F x J F y
50 4 49 biadanii F C Full D G F C Func D G x B y B ran x G y = F x J F y