evlf1

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

	Ref	Expression
Hypotheses	evlf1.e	⊢ 𝐸 = ( 𝐶 eval_F 𝐷 )
	evlf1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	evlf1.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	evlf1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	evlf1.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	evlf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	evlf1	⊢ ( 𝜑 → ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		evlf1.e	⊢ 𝐸 = ( 𝐶 eval_F 𝐷 )
2		evlf1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		evlf1.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
4		evlf1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
5		evlf1.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
6		evlf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
8		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
9		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
10	1 2 3 4 7 8 9	evlfval	⊢ ( 𝜑 → 𝐸 = ⟨ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ 𝐵 ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) , ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × 𝐵 ) , 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × 𝐵 ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) ⟩ )
11		ovex	⊢ ( 𝐶 Func 𝐷 ) ∈ V
12	4	fvexi	⊢ 𝐵 ∈ V
13	11 12	mpoex	⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ 𝐵 ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ∈ V
14	11 12	xpex	⊢ ( ( 𝐶 Func 𝐷 ) × 𝐵 ) ∈ V
15	14 14	mpoex	⊢ ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × 𝐵 ) , 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × 𝐵 ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) ∈ V
16	13 15	op1std	⊢ ( 𝐸 = ⟨ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ 𝐵 ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) , ( 𝑥 ∈ ( ( 𝐶 Func 𝐷 ) × 𝐵 ) , 𝑦 ∈ ( ( 𝐶 Func 𝐷 ) × 𝐵 ) ↦ ⦋ ( 1^st ‘ 𝑥 ) / 𝑚 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑛 ⦌ ( 𝑎 ∈ ( 𝑚 ( 𝐶 Nat 𝐷 ) 𝑛 ) , 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ↦ ( ( 𝑎 ‘ ( 2^nd ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑚 ) ‘ ( 2^nd ‘ 𝑦 ) ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑛 ) ‘ ( 2^nd ‘ 𝑦 ) ) ) ( ( ( 2^nd ‘ 𝑥 ) ( 2^nd ‘ 𝑚 ) ( 2^nd ‘ 𝑦 ) ) ‘ 𝑔 ) ) ) ) ⟩ → ( 1^st ‘ 𝐸 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ 𝐵 ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) )
17	10 16	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝐸 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ 𝐵 ↦ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) )
18		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → 𝑓 = 𝐹 )
19	18	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( 1^st ‘ 𝑓 ) = ( 1^st ‘ 𝐹 ) )
20		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → 𝑥 = 𝑋 )
21	19 20	fveq12d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
22		fvexd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ∈ V )
23	17 21 5 6 22	ovmpod	⊢ ( 𝜑 → ( 𝐹 ( 1^st ‘ 𝐸 ) 𝑋 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )

Metamath Proof Explorer

Theorem evlf1

Proof