Metamath Proof Explorer

Theorem fullfunc

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

Ref Expression
Assertion fullfunc ⊢ C Full D ⊆ C Func D

Proof

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