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	$⊢ φ \to F (C Full D) G$
	fullfo.x	$⊢ φ \to X \in B$
	fullfo.y	$⊢ φ \to Y \in B$
Assertion	fullfo	$⊢ φ \to (X G Y) : X H Y \underset{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	$⊢ φ \to F (C Full D) G$
5		fullfo.x	$⊢ φ \to X \in B$
6		fullfo.y	$⊢ φ \to Y \in B$
7	1 2 3	isfull2	$⊢ F (C Full D) G \leftrightarrow (F (C Func D) G \land \forall x \in B \forall y \in B (x G y) : x H y \underset{onto}{⟶} F (x) J F (y))$
8	7	simprbi	$⊢ F (C Full D) G \to \forall x \in B \forall y \in B (x G y) : x H y \underset{onto}{⟶} F (x) J F (y)$
9	4 8	syl	$⊢ φ \to \forall x \in B \forall y \in B (x G y) : x H y \underset{onto}{⟶} F (x) J F (y)$
10	6	adantr	$⊢ (φ \land x = X) \to Y \in B$
11		simplr	$⊢ ((φ \land x = X) \land y = Y) \to x = X$
12		simpr	$⊢ ((φ \land x = X) \land y = Y) \to y = Y$
13	11 12	oveq12d	$⊢ ((φ \land x = X) \land y = Y) \to x G y = X G Y$
14	11 12	oveq12d	$⊢ ((φ \land x = X) \land y = Y) \to x H y = X H Y$
15	11	fveq2d	$⊢ ((φ \land x = X) \land y = Y) \to F (x) = F (X)$
16	12	fveq2d	$⊢ ((φ \land x = X) \land y = Y) \to F (y) = F (Y)$
17	15 16	oveq12d	$⊢ ((φ \land x = X) \land y = Y) \to F (x) J F (y) = F (X) J F (Y)$
18	13 14 17	foeq123d	$⊢ ((φ \land x = X) \land y = Y) \to ((x G y) : x H y \underset{onto}{⟶} F (x) J F (y) \leftrightarrow (X G Y) : X H Y \underset{onto}{⟶} F (X) J F (Y))$
19	10 18	rspcdv	$⊢ (φ \land x = X) \to (\forall y \in B (x G y) : x H y \underset{onto}{⟶} F (x) J F (y) \to (X G Y) : X H Y \underset{onto}{⟶} F (X) J F (Y))$
20	5 19	rspcimdv	$⊢ φ \to (\forall x \in B \forall y \in B (x G y) : x H y \underset{onto}{⟶} F (x) J F (y) \to (X G Y) : X H Y \underset{onto}{⟶} F (X) J F (Y))$
21	9 20	mpd	$⊢ φ \to (X G Y) : X H Y \underset{onto}{⟶} F (X) J F (Y)$

Metamath Proof Explorer

Theorem fullfo

Proof