evlf1

Description: Value of the evaluation functor at an object. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	evlf1.e	$⊢ E = C {eval}_{F} D$
	evlf1.c	$⊢ φ \to C \in Cat$
	evlf1.d	$⊢ φ \to D \in Cat$
	evlf1.b	$⊢ B = {Base}_{C}$
	evlf1.f	$⊢ φ \to F \in (C Func D)$
	evlf1.x	$⊢ φ \to X \in B$
Assertion	evlf1	$⊢ φ \to F 1^{st} (E) X = 1^{st} (F) (X)$

Proof

Step	Hyp	Ref	Expression
1		evlf1.e	$⊢ E = C {eval}_{F} D$
2		evlf1.c	$⊢ φ \to C \in Cat$
3		evlf1.d	$⊢ φ \to D \in Cat$
4		evlf1.b	$⊢ B = {Base}_{C}$
5		evlf1.f	$⊢ φ \to F \in (C Func D)$
6		evlf1.x	$⊢ φ \to X \in B$
7		eqid	$⊢ Hom (C) = Hom (C)$
8		eqid	$⊢ comp (D) = comp (D)$
9		eqid	$⊢ C Nat D = C Nat D$
10	1 2 3 4 7 8 9	evlfval	$⊢ φ \to E = ⟨(f \in (C Func D), x \in B ⟼ 1^{st} (f) (x)), (x \in ((C Func D) \times B), y \in ((C Func D) \times B) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩$
11		ovex	$⊢ C Func D \in V$
12	4	fvexi	$⊢ B \in V$
13	11 12	mpoex	$⊢ (f \in (C Func D), x \in B ⟼ 1^{st} (f) (x)) \in V$
14	11 12	xpex	$⊢ (C Func D) \times B \in V$
15	14 14	mpoex	$⊢ (x \in ((C Func D) \times B), y \in ((C Func D) \times B) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g))) \in V$
16	13 15	op1std	$⊢ E = ⟨(f \in (C Func D), x \in B ⟼ 1^{st} (f) (x)), (x \in ((C Func D) \times B), y \in ((C Func D) \times B) ⟼ ⦋ 1^{st} (x) / m ⦌ ⦋ 1^{st} (y) / n ⦌ (a \in (m (C Nat D) n), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ a (2^{nd} (y)) (⟨1^{st} (m) (2^{nd} (x)), 1^{st} (m) (2^{nd} (y))⟩ comp (D) 1^{st} (n) (2^{nd} (y))) (2^{nd} (x) 2^{nd} (m) 2^{nd} (y)) (g)))⟩ \to 1^{st} (E) = (f \in (C Func D), x \in B ⟼ 1^{st} (f) (x))$
17	10 16	syl	$⊢ φ \to 1^{st} (E) = (f \in (C Func D), x \in B ⟼ 1^{st} (f) (x))$
18		simprl	$⊢ (φ \land (f = F \land x = X)) \to f = F$
19	18	fveq2d	$⊢ (φ \land (f = F \land x = X)) \to 1^{st} (f) = 1^{st} (F)$
20		simprr	$⊢ (φ \land (f = F \land x = X)) \to x = X$
21	19 20	fveq12d	$⊢ (φ \land (f = F \land x = X)) \to 1^{st} (f) (x) = 1^{st} (F) (X)$
22		fvexd	$⊢ φ \to 1^{st} (F) (X) \in V$
23	17 21 5 6 22	ovmpod	$⊢ φ \to F 1^{st} (E) X = 1^{st} (F) (X)$

Metamath Proof Explorer

Theorem evlf1

Proof