Metamath Proof Explorer

Theorem isfull2

Description: Equivalent condition for a full functor. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses isfull.b ⊢B=BaseC
isfull.j ⊢J=Hom⁡D
isfull.h ⊢H=Hom⁡C
Assertion isfull2 ⊢FCFullDG↔FCFuncDG∧∀x∈B∀y∈BxGy:xHy⟶ontoF⁡xJF⁡y

Proof

Step Hyp Ref Expression
1 isfull.b ⊢B=BaseC
2 isfull.j ⊢J=Hom⁡D
3 isfull.h ⊢H=Hom⁡C
4 1 2 isfull ⊢FCFullDG↔FCFuncDG∧∀x∈B∀y∈Bran⁡xGy=F⁡xJF⁡y
5 simpll ⊢FCFuncDG∧x∈B∧y∈B→FCFuncDG
6 simplr ⊢FCFuncDG∧x∈B∧y∈B→x∈B
7 simpr ⊢FCFuncDG∧x∈B∧y∈B→y∈B
8 1 3 2 5 6 7 funcf2 ⊢FCFuncDG∧x∈B∧y∈B→xGy:xHy⟶F⁡xJF⁡y
9 ffn ⊢xGy:xHy⟶F⁡xJF⁡y→xGyFnxHy
10 df-fo ⊢xGy:xHy⟶ontoF⁡xJF⁡y↔xGyFnxHy∧ran⁡xGy=F⁡xJF⁡y
11 10 baib ⊢xGyFnxHy→xGy:xHy⟶ontoF⁡xJF⁡y↔ran⁡xGy=F⁡xJF⁡y
12 8 9 11 3syl ⊢FCFuncDG∧x∈B∧y∈B→xGy:xHy⟶ontoF⁡xJF⁡y↔ran⁡xGy=F⁡xJF⁡y
13 12 ralbidva ⊢FCFuncDG∧x∈B→∀y∈BxGy:xHy⟶ontoF⁡xJF⁡y↔∀y∈Bran⁡xGy=F⁡xJF⁡y
14 13 ralbidva ⊢FCFuncDG→∀x∈B∀y∈BxGy:xHy⟶ontoF⁡xJF⁡y↔∀x∈B∀y∈Bran⁡xGy=F⁡xJF⁡y
15 14 pm5.32i ⊢FCFuncDG∧∀x∈B∀y∈BxGy:xHy⟶ontoF⁡xJF⁡y↔FCFuncDG∧∀x∈B∀y∈Bran⁡xGy=F⁡xJF⁡y
16 4 15 bitr4i ⊢FCFullDG↔FCFuncDG∧∀x∈B∀y∈BxGy:xHy⟶ontoF⁡xJF⁡y