Metamath Proof Explorer

Theorem fthfunc

Description: A faithful functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Assertion fthfunc ⊢ C Faith D ⊆ C Func D

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ c = C → c Faith d = C Faith d
2 oveq1 ⊢ c = C → c Func d = C Func d
3 1 2 sseq12d ⊢ c = C → c Faith d ⊆ c Func d ↔ C Faith d ⊆ C Func d
4 oveq2 ⊢ d = D → C Faith d = C Faith D
5 oveq2 ⊢ d = D → C Func d = C Func D
6 4 5 sseq12d ⊢ d = D → C Faith d ⊆ C Func d ↔ C Faith D ⊆ C Func D
7 ovex ⊢ c Func d ∈ V
8 simpl ⊢ f c Func d g ∧ ∀ x ∈ Base c ∀ y ∈ Base c Fun ⁡ x g y -1 → f c Func d g
9 8 ssopab2i ⊢ 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
10 opabss ⊢ f g | f c Func d g ⊆ c Func d
11 9 10 sstri ⊢ f g | f c Func d g ∧ ∀ x ∈ Base c ∀ y ∈ Base c Fun ⁡ x g y -1 ⊆ c Func d
12 7 11 ssexi ⊢ f g | f c Func d g ∧ ∀ x ∈ Base c ∀ y ∈ Base c Fun ⁡ x g y -1 ∈ V
13 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
14 13 ovmpt4g ⊢ c ∈ Cat ∧ d ∈ Cat ∧ f g | f c Func d g ∧ ∀ x ∈ Base c ∀ y ∈ Base c Fun ⁡ x g y -1 ∈ V → c Faith d = f g | f c Func d g ∧ ∀ x ∈ Base c ∀ y ∈ Base c Fun ⁡ x g y -1
15 12 14 mp3an3 ⊢ c ∈ Cat ∧ d ∈ Cat → c Faith d = f g | f c Func d g ∧ ∀ x ∈ Base c ∀ y ∈ Base c Fun ⁡ x g y -1
16 15 11 eqsstrdi ⊢ c ∈ Cat ∧ d ∈ Cat → c Faith d ⊆ c Func d
17 3 6 16 vtocl2ga ⊢ C ∈ Cat ∧ D ∈ Cat → C Faith D ⊆ C Func D
18 13 mpondm0 ⊢ ¬ C ∈ Cat ∧ D ∈ Cat → C Faith D = ∅
19 0ss ⊢ ∅ ⊆ C Func D
20 18 19 eqsstrdi ⊢ ¬ C ∈ Cat ∧ D ∈ Cat → C Faith D ⊆ C Func D
21 17 20 pm2.61i ⊢ C Faith D ⊆ C Func D