funcf2

Description: The morphism part of a functor is a function on homsets. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	funcixp.b	$⊢ B = {Base}_{D}$
	funcixp.h	$⊢ H = Hom (D)$
	funcixp.j	$⊢ J = Hom (E)$
	funcixp.f	$⊢ φ \to F (D Func E) G$
	funcf2.x	$⊢ φ \to X \in B$
	funcf2.y	$⊢ φ \to Y \in B$
Assertion	funcf2	$⊢ φ \to (X G Y) : X H Y ⟶ F (X) J F (Y)$

Proof

Step	Hyp	Ref	Expression
1		funcixp.b	$⊢ B = {Base}_{D}$
2		funcixp.h	$⊢ H = Hom (D)$
3		funcixp.j	$⊢ J = Hom (E)$
4		funcixp.f	$⊢ φ \to F (D Func E) G$
5		funcf2.x	$⊢ φ \to X \in B$
6		funcf2.y	$⊢ φ \to Y \in B$
7		df-ov	$⊢ X G Y = G (⟨X, Y⟩)$
8	1 2 3 4	funcixp	$⊢ φ \to G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)})$
9	5 6	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (B \times B)$
10		2fveq3	$⊢ z = ⟨X, Y⟩ \to F (1^{st} (z)) = F (1^{st} (⟨X, Y⟩))$
11		2fveq3	$⊢ z = ⟨X, Y⟩ \to F (2^{nd} (z)) = F (2^{nd} (⟨X, Y⟩))$
12	10 11	oveq12d	$⊢ z = ⟨X, Y⟩ \to F (1^{st} (z)) J F (2^{nd} (z)) = F (1^{st} (⟨X, Y⟩)) J F (2^{nd} (⟨X, Y⟩))$
13		fveq2	$⊢ z = ⟨X, Y⟩ \to H (z) = H (⟨X, Y⟩)$
14		df-ov	$⊢ X H Y = H (⟨X, Y⟩)$
15	13 14	eqtr4di	$⊢ z = ⟨X, Y⟩ \to H (z) = X H Y$
16	12 15	oveq12d	$⊢ z = ⟨X, Y⟩ \to {(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)} = {(F (1^{st} (⟨X, Y⟩)) J F (2^{nd} (⟨X, Y⟩)))}^{(X H Y)}$
17	16	fvixp	$⊢ (G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \land ⟨X, Y⟩ \in (B \times B)) \to G (⟨X, Y⟩) \in ({(F (1^{st} (⟨X, Y⟩)) J F (2^{nd} (⟨X, Y⟩)))}^{(X H Y)})$
18	8 9 17	syl2anc	$⊢ φ \to G (⟨X, Y⟩) \in ({(F (1^{st} (⟨X, Y⟩)) J F (2^{nd} (⟨X, Y⟩)))}^{(X H Y)})$
19	7 18	eqeltrid	$⊢ φ \to X G Y \in ({(F (1^{st} (⟨X, Y⟩)) J F (2^{nd} (⟨X, Y⟩)))}^{(X H Y)})$
20		op1stg	$⊢ (X \in B \land Y \in B) \to 1^{st} (⟨X, Y⟩) = X$
21	20	fveq2d	$⊢ (X \in B \land Y \in B) \to F (1^{st} (⟨X, Y⟩)) = F (X)$
22		op2ndg	$⊢ (X \in B \land Y \in B) \to 2^{nd} (⟨X, Y⟩) = Y$
23	22	fveq2d	$⊢ (X \in B \land Y \in B) \to F (2^{nd} (⟨X, Y⟩)) = F (Y)$
24	21 23	oveq12d	$⊢ (X \in B \land Y \in B) \to F (1^{st} (⟨X, Y⟩)) J F (2^{nd} (⟨X, Y⟩)) = F (X) J F (Y)$
25	5 6 24	syl2anc	$⊢ φ \to F (1^{st} (⟨X, Y⟩)) J F (2^{nd} (⟨X, Y⟩)) = F (X) J F (Y)$
26	25	oveq1d	$⊢ φ \to {(F (1^{st} (⟨X, Y⟩)) J F (2^{nd} (⟨X, Y⟩)))}^{(X H Y)} = {(F (X) J F (Y))}^{(X H Y)}$
27	19 26	eleqtrd	$⊢ φ \to X G Y \in ({(F (X) J F (Y))}^{(X H Y)})$
28		elmapi	$⊢ X G Y \in ({(F (X) J F (Y))}^{(X H Y)}) \to (X G Y) : X H Y ⟶ F (X) J F (Y)$
29	27 28	syl	$⊢ φ \to (X G Y) : X H Y ⟶ F (X) J F (Y)$

Metamath Proof Explorer

Theorem funcf2

Proof