1stf2

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 )
	1stfval.p	⊢ 𝑃 = ( 𝐶 1^st_F 𝐷 )
	1stf1.p	⊢ ( 𝜑 → 𝑅 ∈ 𝐵 )
	1stf2.p	⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
Assertion	1stf2	⊢ ( 𝜑 → ( 𝑅 ( 2^nd ‘ 𝑃 ) 𝑆 ) = ( 1^st ↾ ( 𝑅 𝐻 𝑆 ) ) )

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		1stfval.p	⊢ 𝑃 = ( 𝐶 1^st_F 𝐷 )
7		1stf1.p	⊢ ( 𝜑 → 𝑅 ∈ 𝐵 )
8		1stf2.p	⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
9	1 2 3 4 5 6	1stfval	⊢ ( 𝜑 → 𝑃 = ⟨ ( 1^st ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 1^st ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )
10		fo1st	⊢ 1^st : V –onto→ V
11		fofun	⊢ ( 1^st : V –onto→ V → Fun 1^st )
12	10 11	ax-mp	⊢ Fun 1^st
13	2	fvexi	⊢ 𝐵 ∈ V
14		resfunexg	⊢ ( ( Fun 1^st ∧ 𝐵 ∈ V ) → ( 1^st ↾ 𝐵 ) ∈ V )
15	12 13 14	mp2an	⊢ ( 1^st ↾ 𝐵 ) ∈ V
16	13 13	mpoex	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 1^st ↾ ( 𝑥 𝐻 𝑦 ) ) ) ∈ V
17	15 16	op2ndd	⊢ ( 𝑃 = ⟨ ( 1^st ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 1^st ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ → ( 2^nd ‘ 𝑃 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 1^st ↾ ( 𝑥 𝐻 𝑦 ) ) ) )
18	9 17	syl	⊢ ( 𝜑 → ( 2^nd ‘ 𝑃 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 1^st ↾ ( 𝑥 𝐻 𝑦 ) ) ) )
19		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → 𝑥 = 𝑅 )
20		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → 𝑦 = 𝑆 )
21	19 20	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑅 𝐻 𝑆 ) )
22	21	reseq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → ( 1^st ↾ ( 𝑥 𝐻 𝑦 ) ) = ( 1^st ↾ ( 𝑅 𝐻 𝑆 ) ) )
23		ovex	⊢ ( 𝑅 𝐻 𝑆 ) ∈ V
24		resfunexg	⊢ ( ( Fun 1^st ∧ ( 𝑅 𝐻 𝑆 ) ∈ V ) → ( 1^st ↾ ( 𝑅 𝐻 𝑆 ) ) ∈ V )
25	12 23 24	mp2an	⊢ ( 1^st ↾ ( 𝑅 𝐻 𝑆 ) ) ∈ V
26	25	a1i	⊢ ( 𝜑 → ( 1^st ↾ ( 𝑅 𝐻 𝑆 ) ) ∈ V )
27	18 22 7 8 26	ovmpod	⊢ ( 𝜑 → ( 𝑅 ( 2^nd ‘ 𝑃 ) 𝑆 ) = ( 1^st ↾ ( 𝑅 𝐻 𝑆 ) ) )

Metamath Proof Explorer

Theorem 1stf2

Proof