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=BaseC
isfull.j ⊢J=Hom⁡D
Assertion isfull ⊢FCFullDG↔FCFuncDG∧∀x∈B∀y∈Bran⁡xGy=F⁡xJF⁡y

Proof

Step Hyp Ref Expression
1 isfull.b ⊢B=BaseC
2 isfull.j ⊢J=Hom⁡D
3 fullfunc ⊢CFullD⊆CFuncD
4 3 ssbri ⊢FCFullDG→FCFuncDG
5 df-br ⊢FCFuncDG↔FG∈CFuncD
6 funcrcl ⊢FG∈CFuncD→C∈Cat∧D∈Cat
7 5 6 sylbi ⊢FCFuncDG→C∈Cat∧D∈Cat
8 oveq12 ⊢c=C∧d=D→cFuncd=CFuncD
9 8 breqd ⊢c=C∧d=D→fcFuncdg↔fCFuncDg
10 simpl ⊢c=C∧d=D→c=C
11 10 fveq2d ⊢c=C∧d=D→Basec=BaseC
12 11 1 eqtr4di ⊢c=C∧d=D→Basec=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⁡xHom⁡df⁡y=f⁡xJf⁡y
17 16 eqeq2d ⊢c=C∧d=D→ran⁡xgy=f⁡xHom⁡df⁡y↔ran⁡xgy=f⁡xJf⁡y
18 12 17 raleqbidv ⊢c=C∧d=D→∀y∈Basecran⁡xgy=f⁡xHom⁡df⁡y↔∀y∈Bran⁡xgy=f⁡xJf⁡y
19 12 18 raleqbidv ⊢c=C∧d=D→∀x∈Basec∀y∈Basecran⁡xgy=f⁡xHom⁡df⁡y↔∀x∈B∀y∈Bran⁡xgy=f⁡xJf⁡y
20 9 19 anbi12d ⊢c=C∧d=D→fcFuncdg∧∀x∈Basec∀y∈Basecran⁡xgy=f⁡xHom⁡df⁡y↔fCFuncDg∧∀x∈B∀y∈Bran⁡xgy=f⁡xJf⁡y
21 20 opabbidv ⊢c=C∧d=D→fg|fcFuncdg∧∀x∈Basec∀y∈Basecran⁡xgy=f⁡xHom⁡df⁡y=fg|fCFuncDg∧∀x∈B∀y∈Bran⁡xgy=f⁡xJf⁡y
22 df-full ⊢Full=c∈Cat,d∈Cat⟼fg|fcFuncdg∧∀x∈Basec∀y∈Basecran⁡xgy=f⁡xHom⁡df⁡y
23 ovex ⊢CFuncD∈V
24 simpl ⊢fCFuncDg∧∀x∈B∀y∈Bran⁡xgy=f⁡xJf⁡y→fCFuncDg
25 24 ssopab2i ⊢fg|fCFuncDg∧∀x∈B∀y∈Bran⁡xgy=f⁡xJf⁡y⊆fg|fCFuncDg
26 opabss ⊢fg|fCFuncDg⊆CFuncD
27 25 26 sstri ⊢fg|fCFuncDg∧∀x∈B∀y∈Bran⁡xgy=f⁡xJf⁡y⊆CFuncD
28 23 27 ssexi ⊢fg|fCFuncDg∧∀x∈B∀y∈Bran⁡xgy=f⁡xJf⁡y∈V
29 21 22 28 ovmpoa ⊢C∈Cat∧D∈Cat→CFullD=fg|fCFuncDg∧∀x∈B∀y∈Bran⁡xgy=f⁡xJf⁡y
30 7 29 syl ⊢FCFuncDG→CFullD=fg|fCFuncDg∧∀x∈B∀y∈Bran⁡xgy=f⁡xJf⁡y
31 30 breqd ⊢FCFuncDG→FCFullDG↔Ffg|fCFuncDg∧∀x∈B∀y∈Bran⁡xgy=f⁡xJf⁡yG
32 relfunc ⊢Rel⁡CFuncD
33 32 brrelex12i ⊢FCFuncDG→F∈V∧G∈V
34 breq12 ⊢f=F∧g=G→fCFuncDg↔FCFuncDG
35 simpr ⊢f=F∧g=G→g=G
36 35 oveqd ⊢f=F∧g=G→xgy=xGy
37 36 rneqd ⊢f=F∧g=G→ran⁡xgy=ran⁡xGy
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⁡xJf⁡y=F⁡xJF⁡y
42 37 41 eqeq12d ⊢f=F∧g=G→ran⁡xgy=f⁡xJf⁡y↔ran⁡xGy=F⁡xJF⁡y
43 42 2ralbidv ⊢f=F∧g=G→∀x∈B∀y∈Bran⁡xgy=f⁡xJf⁡y↔∀x∈B∀y∈Bran⁡xGy=F⁡xJF⁡y
44 34 43 anbi12d ⊢f=F∧g=G→fCFuncDg∧∀x∈B∀y∈Bran⁡xgy=f⁡xJf⁡y↔FCFuncDG∧∀x∈B∀y∈Bran⁡xGy=F⁡xJF⁡y
45 eqid ⊢fg|fCFuncDg∧∀x∈B∀y∈Bran⁡xgy=f⁡xJf⁡y=fg|fCFuncDg∧∀x∈B∀y∈Bran⁡xgy=f⁡xJf⁡y
46 44 45 brabga ⊢F∈V∧G∈V→Ffg|fCFuncDg∧∀x∈B∀y∈Bran⁡xgy=f⁡xJf⁡yG↔FCFuncDG∧∀x∈B∀y∈Bran⁡xGy=F⁡xJF⁡y
47 33 46 syl ⊢FCFuncDG→Ffg|fCFuncDg∧∀x∈B∀y∈Bran⁡xgy=f⁡xJf⁡yG↔FCFuncDG∧∀x∈B∀y∈Bran⁡xGy=F⁡xJF⁡y
48 31 47 bitrd ⊢FCFuncDG→FCFullDG↔FCFuncDG∧∀x∈B∀y∈Bran⁡xGy=F⁡xJF⁡y
49 48 bianabs ⊢FCFuncDG→FCFullDG↔∀x∈B∀y∈Bran⁡xGy=F⁡xJF⁡y
50 4 49 biadanii ⊢FCFullDG↔FCFuncDG∧∀x∈B∀y∈Bran⁡xGy=F⁡xJF⁡y