This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fulli

Description: The morphism map of a full functor is a surjection. (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
fullfo.f ⊢ φ → F C Full D G
fullfo.x ⊢ φ → X ∈ B
fullfo.y ⊢ φ → Y ∈ B
fulli.r ⊢ φ → R ∈ F ⁡ X J F ⁡ Y
Assertion fulli ⊢ φ → ∃ f ∈ X H Y R = X G Y ⁡ f

Proof

Step Hyp Ref Expression
1 isfull.b ⊢ B = Base C
2 isfull.j ⊢ J = Hom ⁡ D
3 isfull.h ⊢ H = Hom ⁡ C
4 fullfo.f ⊢ φ → F C Full D G
5 fullfo.x ⊢ φ → X ∈ B
6 fullfo.y ⊢ φ → Y ∈ B
7 fulli.r ⊢ φ → R ∈ F ⁡ X J F ⁡ Y
8 1 2 3 4 5 6 fullfo ⊢ φ → X G Y : X H Y ⟶ onto F ⁡ X J F ⁡ Y
9 foelrn ⊢ X G Y : X H Y ⟶ onto F ⁡ X J F ⁡ Y ∧ R ∈ F ⁡ X J F ⁡ Y → ∃ f ∈ X H Y R = X G Y ⁡ f
10 8 7 9 syl2anc ⊢ φ → ∃ f ∈ X H Y R = X G Y ⁡ f