curf11

Description: Value of the double evaluated curry functor. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	curfval.g	⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 )
	curfval.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	curfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	curfval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	curfval.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
	curfval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	curf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	curf1.k	⊢ 𝐾 = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 )
	curf11.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	curf11	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) = ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		curfval.g	⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 )
2		curfval.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		curfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		curfval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
5		curfval.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
6		curfval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
7		curf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
8		curf1.k	⊢ 𝐾 = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 )
9		curf11.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
10		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
11		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
12	1 2 3 4 5 6 7 8 10 11	curf1	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ )
13	6	fvexi	⊢ 𝐵 ∈ V
14	13	mptex	⊢ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) ∈ V
15	13 13	mpoex	⊢ ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ∈ V
16	14 15	op1std	⊢ ( 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ → ( 1^st ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) )
17	12 16	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) )
18		simpr	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
19	18	oveq2d	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑌 ) → ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) = ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑌 ) )
20		ovexd	⊢ ( 𝜑 → ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑌 ) ∈ V )
21	17 19 9 20	fvmptd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) = ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑌 ) )

Metamath Proof Explorer

Theorem curf11

Proof