Theorem 2ndf1

Description: Value of the first projection on an object. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	1stfval.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
	1stfval.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
	1stfval.h	⊢ 𝐻 = ( Hom ‘ 𝑇 )
	1stfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	1stfval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	2ndfval.p	⊢ 𝑄 = ( 𝐶 2ndF 𝐷 )
	2ndf1.p	⊢ ( 𝜑 → 𝑅 ∈ 𝐵 )
Assertion	2ndf1	⊢ ( 𝜑 → ( ( 1st ‘ 𝑄 ) ‘ 𝑅 ) = ( 2nd ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		1stfval.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
2		1stfval.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
3		1stfval.h	⊢ 𝐻 = ( Hom ‘ 𝑇 )
4		1stfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
5		1stfval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
6		2ndfval.p	⊢ 𝑄 = ( 𝐶 2ndF 𝐷 )
7		2ndf1.p	⊢ ( 𝜑 → 𝑅 ∈ 𝐵 )
8	1 2 3 4 5 6	2ndfval	⊢ ( 𝜑 → 𝑄 = ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )
9		fo2nd	⊢ 2nd : V –onto→ V
10		fofun	⊢ ( 2nd : V –onto→ V → Fun 2nd )
11	9 10	ax-mp	⊢ Fun 2nd
12	2	fvexi	⊢ 𝐵 ∈ V
13		resfunexg	⊢ ( ( Fun 2nd ∧ 𝐵 ∈ V ) → ( 2nd ↾ 𝐵 ) ∈ V )
14	11 12 13	mp2an	⊢ ( 2nd ↾ 𝐵 ) ∈ V
15	12 12	mpoex	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ∈ V
16	14 15	op1std	⊢ ( 𝑄 = ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ → ( 1st ‘ 𝑄 ) = ( 2nd ↾ 𝐵 ) )
17	8 16	syl	⊢ ( 𝜑 → ( 1st ‘ 𝑄 ) = ( 2nd ↾ 𝐵 ) )
18	17	fveq1d	⊢ ( 𝜑 → ( ( 1st ‘ 𝑄 ) ‘ 𝑅 ) = ( ( 2nd ↾ 𝐵 ) ‘ 𝑅 ) )
19	7	fvresd	⊢ ( 𝜑 → ( ( 2nd ↾ 𝐵 ) ‘ 𝑅 ) = ( 2nd ‘ 𝑅 ) )
20	18 19	eqtrd	⊢ ( 𝜑 → ( ( 1st ‘ 𝑄 ) ‘ 𝑅 ) = ( 2nd ‘ 𝑅 ) )