This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑅 ) )