comfffval

Description: Value of the functionalized composition operation. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

	Ref	Expression
Hypotheses	comfffval.o	$⊢ O = {comp}_{𝑓} (C)$
	comfffval.b	$⊢ B = {Base}_{C}$
	comfffval.h	$⊢ H = Hom (C)$
	comfffval.x	$⊢ \underset{˙}{\cdot} = comp (C)$
Assertion	comfffval	$⊢ O = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) H y), f \in H (x) ⟼ g (x \underset{˙}{\cdot} y) f))$

Proof

Step	Hyp	Ref	Expression
1		comfffval.o	$⊢ O = {comp}_{𝑓} (C)$
2		comfffval.b	$⊢ B = {Base}_{C}$
3		comfffval.h	$⊢ H = Hom (C)$
4		comfffval.x	$⊢ \underset{˙}{\cdot} = comp (C)$
5		fveq2	$⊢ c = C \to {Base}_{c} = {Base}_{C}$
6	5 2	eqtr4di	$⊢ c = C \to {Base}_{c} = B$
7	6	sqxpeqd	$⊢ c = C \to {Base}_{c} \times {Base}_{c} = B \times B$
8		fveq2	$⊢ c = C \to Hom (c) = Hom (C)$
9	8 3	eqtr4di	$⊢ c = C \to Hom (c) = H$
10	9	oveqd	$⊢ c = C \to 2^{nd} (x) Hom (c) y = 2^{nd} (x) H y$
11	9	fveq1d	$⊢ c = C \to Hom (c) (x) = H (x)$
12		fveq2	$⊢ c = C \to comp (c) = comp (C)$
13	12 4	eqtr4di	$⊢ c = C \to comp (c) = \underset{˙}{\cdot}$
14	13	oveqd	$⊢ c = C \to x comp (c) y = x \underset{˙}{\cdot} y$
15	14	oveqd	$⊢ c = C \to g (x comp (c) y) f = g (x \underset{˙}{\cdot} y) f$
16	10 11 15	mpoeq123dv	$⊢ c = C \to (g \in (2^{nd} (x) Hom (c) y), f \in Hom (c) (x) ⟼ g (x comp (c) y) f) = (g \in (2^{nd} (x) H y), f \in H (x) ⟼ g (x \underset{˙}{\cdot} y) f)$
17	7 6 16	mpoeq123dv	$⊢ c = C \to (x \in ({Base}_{c} \times {Base}_{c}), y \in {Base}_{c} ⟼ (g \in (2^{nd} (x) Hom (c) y), f \in Hom (c) (x) ⟼ g (x comp (c) y) f)) = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) H y), f \in H (x) ⟼ g (x \underset{˙}{\cdot} y) f))$
18		df-comf	$⊢ {comp}_{𝑓} = (c \in V ⟼ (x \in ({Base}_{c} \times {Base}_{c}), y \in {Base}_{c} ⟼ (g \in (2^{nd} (x) Hom (c) y), f \in Hom (c) (x) ⟼ g (x comp (c) y) f)))$
19	2	fvexi	$⊢ B \in V$
20	19 19	xpex	$⊢ B \times B \in V$
21	20 19	mpoex	$⊢ (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) H y), f \in H (x) ⟼ g (x \underset{˙}{\cdot} y) f)) \in V$
22	17 18 21	fvmpt	$⊢ C \in V \to {comp}_{𝑓} (C) = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) H y), f \in H (x) ⟼ g (x \underset{˙}{\cdot} y) f))$
23		fvprc	$⊢ \neg C \in V \to {comp}_{𝑓} (C) = \emptyset$
24		fvprc	$⊢ \neg C \in V \to {Base}_{C} = \emptyset$
25	2 24	syl5eq	$⊢ \neg C \in V \to B = \emptyset$
26	25	olcd	$⊢ \neg C \in V \to (B \times B = \emptyset \lor B = \emptyset)$
27		0mpo0	$⊢ (B \times B = \emptyset \lor B = \emptyset) \to (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) H y), f \in H (x) ⟼ g (x \underset{˙}{\cdot} y) f)) = \emptyset$
28	26 27	syl	$⊢ \neg C \in V \to (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) H y), f \in H (x) ⟼ g (x \underset{˙}{\cdot} y) f)) = \emptyset$
29	23 28	eqtr4d	$⊢ \neg C \in V \to {comp}_{𝑓} (C) = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) H y), f \in H (x) ⟼ g (x \underset{˙}{\cdot} y) f))$
30	22 29	pm2.61i	$⊢ {comp}_{𝑓} (C) = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) H y), f \in H (x) ⟼ g (x \underset{˙}{\cdot} y) f))$
31	1 30	eqtri	$⊢ O = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) H y), f \in H (x) ⟼ g (x \underset{˙}{\cdot} y) f))$

Metamath Proof Explorer

Theorem comfffval

Proof