Metamath Proof Explorer


Theorem diag11

Description: Value of the constant functor at an object. (Contributed by Mario Carneiro, 7-Jan-2017) (Revised by Mario Carneiro, 15-Jan-2017)

Ref Expression
Hypotheses diagval.l 𝐿 = ( 𝐶 Δfunc 𝐷 )
diagval.c ( 𝜑𝐶 ∈ Cat )
diagval.d ( 𝜑𝐷 ∈ Cat )
diag11.a 𝐴 = ( Base ‘ 𝐶 )
diag11.c ( 𝜑𝑋𝐴 )
diag11.k 𝐾 = ( ( 1st𝐿 ) ‘ 𝑋 )
diag11.b 𝐵 = ( Base ‘ 𝐷 )
diag11.y ( 𝜑𝑌𝐵 )
Assertion diag11 ( 𝜑 → ( ( 1st𝐾 ) ‘ 𝑌 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 diagval.l 𝐿 = ( 𝐶 Δfunc 𝐷 )
2 diagval.c ( 𝜑𝐶 ∈ Cat )
3 diagval.d ( 𝜑𝐷 ∈ Cat )
4 diag11.a 𝐴 = ( Base ‘ 𝐶 )
5 diag11.c ( 𝜑𝑋𝐴 )
6 diag11.k 𝐾 = ( ( 1st𝐿 ) ‘ 𝑋 )
7 diag11.b 𝐵 = ( Base ‘ 𝐷 )
8 diag11.y ( 𝜑𝑌𝐵 )
9 1 2 3 diagval ( 𝜑𝐿 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) )
10 9 fveq2d ( 𝜑 → ( 1st𝐿 ) = ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) )
11 10 fveq1d ( 𝜑 → ( ( 1st𝐿 ) ‘ 𝑋 ) = ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) ‘ 𝑋 ) )
12 6 11 eqtrid ( 𝜑𝐾 = ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) ‘ 𝑋 ) )
13 12 fveq2d ( 𝜑 → ( 1st𝐾 ) = ( 1st ‘ ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) ‘ 𝑋 ) ) )
14 13 fveq1d ( 𝜑 → ( ( 1st𝐾 ) ‘ 𝑌 ) = ( ( 1st ‘ ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) ‘ 𝑋 ) ) ‘ 𝑌 ) )
15 eqid ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) )
16 eqid ( 𝐶 ×c 𝐷 ) = ( 𝐶 ×c 𝐷 )
17 eqid ( 𝐶 1stF 𝐷 ) = ( 𝐶 1stF 𝐷 )
18 16 2 3 17 1stfcl ( 𝜑 → ( 𝐶 1stF 𝐷 ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐶 ) )
19 eqid ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) ‘ 𝑋 ) = ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) ‘ 𝑋 )
20 15 4 2 3 18 7 5 19 8 curf11 ( 𝜑 → ( ( 1st ‘ ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 1stF 𝐷 ) ) ) ‘ 𝑋 ) ) ‘ 𝑌 ) = ( 𝑋 ( 1st ‘ ( 𝐶 1stF 𝐷 ) ) 𝑌 ) )
21 df-ov ( 𝑋 ( 1st ‘ ( 𝐶 1stF 𝐷 ) ) 𝑌 ) = ( ( 1st ‘ ( 𝐶 1stF 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
22 16 4 7 xpcbas ( 𝐴 × 𝐵 ) = ( Base ‘ ( 𝐶 ×c 𝐷 ) )
23 eqid ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×c 𝐷 ) )
24 5 8 opelxpd ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × 𝐵 ) )
25 16 22 23 2 3 17 24 1stf1 ( 𝜑 → ( ( 1st ‘ ( 𝐶 1stF 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
26 21 25 eqtrid ( 𝜑 → ( 𝑋 ( 1st ‘ ( 𝐶 1stF 𝐷 ) ) 𝑌 ) = ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
27 op1stg ( ( 𝑋𝐴𝑌𝐵 ) → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
28 5 8 27 syl2anc ( 𝜑 → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
29 26 28 eqtrd ( 𝜑 → ( 𝑋 ( 1st ‘ ( 𝐶 1stF 𝐷 ) ) 𝑌 ) = 𝑋 )
30 14 20 29 3eqtrd ( 𝜑 → ( ( 1st𝐾 ) ‘ 𝑌 ) = 𝑋 )