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	⊢ 𝐾 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
	diag11.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	diag11.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	diag11	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) = 𝑋 )

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	⊢ 𝐾 = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
7		diag11.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
8		diag11.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9	1 2 3	diagval	⊢ ( 𝜑 → 𝐿 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 1^st_F 𝐷 ) ) )
10	9	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) = ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 1^st_F 𝐷 ) ) ) )
11	10	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) = ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 1^st_F 𝐷 ) ) ) ‘ 𝑋 ) )
12	6 11	eqtrid	⊢ ( 𝜑 → 𝐾 = ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 1^st_F 𝐷 ) ) ) ‘ 𝑋 ) )
13	12	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) = ( 1^st ‘ ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 1^st_F 𝐷 ) ) ) ‘ 𝑋 ) ) )
14	13	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) = ( ( 1^st ‘ ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 1^st_F 𝐷 ) ) ) ‘ 𝑋 ) ) ‘ 𝑌 ) )
15		eqid	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 1^st_F 𝐷 ) ) = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 1^st_F 𝐷 ) )
16		eqid	⊢ ( 𝐶 ×_c 𝐷 ) = ( 𝐶 ×_c 𝐷 )
17		eqid	⊢ ( 𝐶 1^st_F 𝐷 ) = ( 𝐶 1^st_F 𝐷 )
18	16 2 3 17	1stfcl	⊢ ( 𝜑 → ( 𝐶 1^st_F 𝐷 ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐶 ) )
19		eqid	⊢ ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 1^st_F 𝐷 ) ) ) ‘ 𝑋 ) = ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 1^st_F 𝐷 ) ) ) ‘ 𝑋 )
20	15 4 2 3 18 7 5 19 8	curf11	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 1^st_F 𝐷 ) ) ) ‘ 𝑋 ) ) ‘ 𝑌 ) = ( 𝑋 ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) 𝑌 ) )
21		df-ov	⊢ ( 𝑋 ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) 𝑌 ) = ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
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	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
26	21 25	eqtrid	⊢ ( 𝜑 → ( 𝑋 ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) 𝑌 ) = ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
27		op1stg	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
28	5 8 27	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
29	26 28	eqtrd	⊢ ( 𝜑 → ( 𝑋 ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) 𝑌 ) = 𝑋 )
30	14 20 29	3eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑌 ) = 𝑋 )

Metamath Proof Explorer

Theorem diag11

Proof