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