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