1stf1

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

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		1stfval.p	⊢ 𝑃 = ( 𝐶 1^st_F 𝐷 )
7		1stf1.p	⊢ ( 𝜑 → 𝑅 ∈ 𝐵 )
8	1 2 3 4 5 6	1stfval	⊢ ( 𝜑 → 𝑃 = ⟨ ( 1^st ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 1^st ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )
9		fo1st	⊢ 1^st : V –onto→ V
10		fofun	⊢ ( 1^st : V –onto→ V → Fun 1^st )
11	9 10	ax-mp	⊢ Fun 1^st
12	2	fvexi	⊢ 𝐵 ∈ V
13		resfunexg	⊢ ( ( Fun 1^st ∧ 𝐵 ∈ V ) → ( 1^st ↾ 𝐵 ) ∈ V )
14	11 12 13	mp2an	⊢ ( 1^st ↾ 𝐵 ) ∈ V
15	12 12	mpoex	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 1^st ↾ ( 𝑥 𝐻 𝑦 ) ) ) ∈ V
16	14 15	op1std	⊢ ( 𝑃 = ⟨ ( 1^st ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 1^st ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ → ( 1^st ‘ 𝑃 ) = ( 1^st ↾ 𝐵 ) )
17	8 16	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝑃 ) = ( 1^st ↾ 𝐵 ) )
18	17	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑃 ) ‘ 𝑅 ) = ( ( 1^st ↾ 𝐵 ) ‘ 𝑅 ) )
19	7	fvresd	⊢ ( 𝜑 → ( ( 1^st ↾ 𝐵 ) ‘ 𝑅 ) = ( 1^st ‘ 𝑅 ) )
20	18 19	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑃 ) ‘ 𝑅 ) = ( 1^st ‘ 𝑅 ) )

Metamath Proof Explorer