Metamath Proof Explorer


Theorem isfth

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

Ref Expression
Hypothesis isfth.b B = Base C
Assertion isfth F C Faith D G F C Func D G x B y B Fun x G y -1

Proof

Step Hyp Ref Expression
1 isfth.b B = Base C
2 fthfunc C Faith D C Func D
3 2 ssbri F C Faith D G F C Func D G
4 df-br F C Func D G F G C Func D
5 funcrcl F G C Func D C Cat D Cat
6 4 5 sylbi F C Func D G C Cat D Cat
7 oveq12 c = C d = D c Func d = C Func D
8 7 breqd c = C d = D f c Func d g f C Func D g
9 simpl c = C d = D c = C
10 9 fveq2d c = C d = D Base c = Base C
11 10 1 eqtr4di c = C d = D Base c = B
12 11 raleqdv c = C d = D y Base c Fun x g y -1 y B Fun x g y -1
13 11 12 raleqbidv c = C d = D x Base c y Base c Fun x g y -1 x B y B Fun x g y -1
14 8 13 anbi12d c = C d = D f c Func d g x Base c y Base c Fun x g y -1 f C Func D g x B y B Fun x g y -1
15 14 opabbidv c = C d = D f g | f c Func d g x Base c y Base c Fun x g y -1 = f g | f C Func D g x B y B Fun x g y -1
16 df-fth Faith = c Cat , d Cat f g | f c Func d g x Base c y Base c Fun x g y -1
17 ovex C Func D V
18 simpl f C Func D g x B y B Fun x g y -1 f C Func D g
19 18 ssopab2i f g | f C Func D g x B y B Fun x g y -1 f g | f C Func D g
20 opabss f g | f C Func D g C Func D
21 19 20 sstri f g | f C Func D g x B y B Fun x g y -1 C Func D
22 17 21 ssexi f g | f C Func D g x B y B Fun x g y -1 V
23 15 16 22 ovmpoa C Cat D Cat C Faith D = f g | f C Func D g x B y B Fun x g y -1
24 6 23 syl F C Func D G C Faith D = f g | f C Func D g x B y B Fun x g y -1
25 24 breqd F C Func D G F C Faith D G F f g | f C Func D g x B y B Fun x g y -1 G
26 relfunc Rel C Func D
27 26 brrelex12i F C Func D G F V G V
28 breq12 f = F g = G f C Func D g F C Func D G
29 simpr f = F g = G g = G
30 29 oveqd f = F g = G x g y = x G y
31 30 cnveqd f = F g = G x g y -1 = x G y -1
32 31 funeqd f = F g = G Fun x g y -1 Fun x G y -1
33 32 2ralbidv f = F g = G x B y B Fun x g y -1 x B y B Fun x G y -1
34 28 33 anbi12d f = F g = G f C Func D g x B y B Fun x g y -1 F C Func D G x B y B Fun x G y -1
35 eqid f g | f C Func D g x B y B Fun x g y -1 = f g | f C Func D g x B y B Fun x g y -1
36 34 35 brabga F V G V F f g | f C Func D g x B y B Fun x g y -1 G F C Func D G x B y B Fun x G y -1
37 27 36 syl F C Func D G F f g | f C Func D g x B y B Fun x g y -1 G F C Func D G x B y B Fun x G y -1
38 25 37 bitrd F C Func D G F C Faith D G F C Func D G x B y B Fun x G y -1
39 38 bianabs F C Func D G F C Faith D G x B y B Fun x G y -1
40 3 39 biadanii F C Faith D G F C Func D G x B y B Fun x G y -1