curf1

Description: Value of the object part of the 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 ‘ 𝐺 ) ‘ 𝑋 )
	curf1.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	curf1.1	⊢ 1 = ( Id ‘ 𝐶 )
Assertion	curf1	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ )

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		curf1.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
10		curf1.1	⊢ 1 = ( Id ‘ 𝐶 )
11	1 2 3 4 5 6 9 10	curf1fval	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
13	12	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) = ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) )
14	13	mpteq2dv	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) )
15		simp1r	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → 𝑥 = 𝑋 )
16	15	opeq1d	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑋 , 𝑦 ⟩ )
17	15	opeq1d	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑋 , 𝑧 ⟩ )
18	16 17	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) = ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) )
19	15	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 1 ‘ 𝑥 ) = ( 1 ‘ 𝑋 ) )
20		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → 𝑔 = 𝑔 )
21	18 19 20	oveq123d	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) )
22	21	mpteq2dv	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) )
23	22	mpoeq3dva	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) )
24	14 23	opeq12d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ )
25		opex	⊢ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ∈ V
26	25	a1i	⊢ ( 𝜑 → ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ∈ V )
27	11 24 7 26	fvmptd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ )
28	8 27	eqtrid	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ )

Metamath Proof Explorer

Theorem curf1

Proof