Theorem 2ndf2

Description: Value of the first projection on a morphism. (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	⊢ ( 𝜑 → 𝑅 ∈ 𝐵 )
	2ndf2.p	⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
Assertion	2ndf2	⊢ ( 𝜑 → ( 𝑅 ( 2nd ‘ 𝑄 ) 𝑆 ) = ( 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		2ndf2.p	⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
9	1 2 3 4 5 6	2ndfval	⊢ ( 𝜑 → 𝑄 = ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )
10		fo2nd	⊢ 2nd : V –onto→ V
11		fofun	⊢ ( 2nd : V –onto→ V → Fun 2nd )
12	10 11	ax-mp	⊢ Fun 2nd
13	2	fvexi	⊢ 𝐵 ∈ V
14		resfunexg	⊢ ( ( Fun 2nd ∧ 𝐵 ∈ V ) → ( 2nd ↾ 𝐵 ) ∈ V )
15	12 13 14	mp2an	⊢ ( 2nd ↾ 𝐵 ) ∈ V
16	13 13	mpoex	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ∈ V
17	15 16	op2ndd	⊢ ( 𝑄 = ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ → ( 2nd ‘ 𝑄 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) )
18	9 17	syl	⊢ ( 𝜑 → ( 2nd ‘ 𝑄 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) )
19		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → 𝑥 = 𝑅 )
20		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → 𝑦 = 𝑆 )
21	19 20	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑅 𝐻 𝑆 ) )
22	21	reseq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) = ( 2nd ↾ ( 𝑅 𝐻 𝑆 ) ) )
23		ovex	⊢ ( 𝑅 𝐻 𝑆 ) ∈ V
24		resfunexg	⊢ ( ( Fun 2nd ∧ ( 𝑅 𝐻 𝑆 ) ∈ V ) → ( 2nd ↾ ( 𝑅 𝐻 𝑆 ) ) ∈ V )
25	12 23 24	mp2an	⊢ ( 2nd ↾ ( 𝑅 𝐻 𝑆 ) ) ∈ V
26	25	a1i	⊢ ( 𝜑 → ( 2nd ↾ ( 𝑅 𝐻 𝑆 ) ) ∈ V )
27	18 22 7 8 26	ovmpod	⊢ ( 𝜑 → ( 𝑅 ( 2nd ‘ 𝑄 ) 𝑆 ) = ( 2nd ↾ ( 𝑅 𝐻 𝑆 ) ) )