Metamath Proof Explorer

Theorem fullfo

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
Assertion fullfo ⊢ φ → 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 fullfo.f ⊢ φ → F C Full D G
5 fullfo.x ⊢ φ → X ∈ B
6 fullfo.y ⊢ φ → Y ∈ B
7 1 2 3 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
8 7 simprbi ⊢ F C Full D G → ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y
9 4 8 syl ⊢ φ → ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y
10 6 adantr ⊢ φ ∧ x = X → Y ∈ B
11 simplr ⊢ φ ∧ x = X ∧ y = Y → x = X
12 simpr ⊢ φ ∧ x = X ∧ y = Y → y = Y
13 11 12 oveq12d ⊢ φ ∧ x = X ∧ y = Y → x G y = X G Y
14 11 12 oveq12d ⊢ φ ∧ x = X ∧ y = Y → x H y = X H Y
15 11 fveq2d ⊢ φ ∧ x = X ∧ y = Y → F ⁡ x = F ⁡ X
16 12 fveq2d ⊢ φ ∧ x = X ∧ y = Y → F ⁡ y = F ⁡ Y
17 15 16 oveq12d ⊢ φ ∧ x = X ∧ y = Y → F ⁡ x J F ⁡ y = F ⁡ X J F ⁡ Y
18 13 14 17 foeq123d ⊢ φ ∧ x = X ∧ y = Y → x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ↔ X G Y : X H Y ⟶ onto F ⁡ X J F ⁡ Y
19 10 18 rspcdv ⊢ φ ∧ x = X → ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y → X G Y : X H Y ⟶ onto F ⁡ X J F ⁡ Y
20 5 19 rspcimdv ⊢ φ → ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y → X G Y : X H Y ⟶ onto F ⁡ X J F ⁡ Y
21 9 20 mpd ⊢ φ → X G Y : X H Y ⟶ onto F ⁡ X J F ⁡ Y