Metamath Proof Explorer

Theorem curf1fval

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 ‘ 𝐷 )
		curfval.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
		curfval.1	⊢ 1 = ( Id ‘ 𝐶 )
	Assertion	curf1fval	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 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		curfval.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
8		curfval.1	⊢ 1 = ( Id ‘ 𝐶 )
9		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
10		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
11	1 2 3 4 5 6 7 8 9 10	curfval	⊢ ( 𝜑 → 𝐺 = ⟨ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ⟩ )
12	2	fvexi	⊢ 𝐴 ∈ V
13	12	mptex	⊢ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) ∈ V
14	12 12	mpoex	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ∈ V
15	13 14	op1std	⊢ ( 𝐺 = ⟨ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ⟩ → ( 1^st ‘ 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) )
16	11 15	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) )