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