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 = Base C
isfull.j ⊢ J = Hom ⁡ D
isfull.h ⊢ H = Hom ⁡ C
Assertion isfull2 ⊢ F C Full D G ↔ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y

Proof

Step Hyp Ref Expression
1 isfull.b ⊢ B = Base C
2 isfull.j ⊢ J = Hom ⁡ D
3 isfull.h ⊢ H = Hom ⁡ C
4 1 2 isfull ⊢ F C Full D G ↔ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B ran ⁡ x G y = F ⁡ x J F ⁡ y
5 simpll ⊢ F C Func D G ∧ x ∈ B ∧ y ∈ B → F C Func D G
6 simplr ⊢ F C Func D G ∧ x ∈ B ∧ y ∈ B → x ∈ B
7 simpr ⊢ F C Func D G ∧ x ∈ B ∧ y ∈ B → y ∈ B
8 1 3 2 5 6 7 funcf2 ⊢ F C Func D G ∧ x ∈ B ∧ y ∈ B → x G y : x H y ⟶ F ⁡ x J F ⁡ y
9 ffn ⊢ x G y : x H y ⟶ F ⁡ x J F ⁡ y → x G y Fn x H y
10 df-fo ⊢ x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ↔ x G y Fn x H y ∧ ran ⁡ x G y = F ⁡ x J F ⁡ y
11 10 baib ⊢ x G y Fn x H y → x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ↔ ran ⁡ x G y = F ⁡ x J F ⁡ y
12 8 9 11 3syl ⊢ F C Func D G ∧ x ∈ B ∧ y ∈ B → x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ↔ ran ⁡ x G y = F ⁡ x J F ⁡ y
13 12 ralbidva ⊢ F C Func D G ∧ x ∈ B → ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ↔ ∀ y ∈ B ran ⁡ x G y = F ⁡ x J F ⁡ y
14 13 ralbidva ⊢ F C Func D G → ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ↔ ∀ x ∈ B ∀ y ∈ B ran ⁡ x G y = F ⁡ x J F ⁡ y
15 14 pm5.32i ⊢ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ↔ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B ran ⁡ x G y = F ⁡ x J F ⁡ y
16 4 15 bitr4i ⊢ F C Full D G ↔ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y