Theorem idfu2nd

Description: Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	idfuval.i	⊢ 𝐼 = ( idfunc ‘ 𝐶 )
	idfuval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	idfuval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	idfuval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	idfu2nd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	idfu2nd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	idfu2nd	⊢ ( 𝜑 → ( 𝑋 ( 2nd ‘ 𝐼 ) 𝑌 ) = ( I ↾ ( 𝑋 𝐻 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		idfuval.i	⊢ 𝐼 = ( idfunc ‘ 𝐶 )
2		idfuval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		idfuval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		idfuval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
5		idfu2nd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		idfu2nd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		df-ov	⊢ ( 𝑋 ( 2nd ‘ 𝐼 ) 𝑌 ) = ( ( 2nd ‘ 𝐼 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
8	1 2 3 4	idfuval	⊢ ( 𝜑 → 𝐼 = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ )
9	8	fveq2d	⊢ ( 𝜑 → ( 2nd ‘ 𝐼 ) = ( 2nd ‘ ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ) )
10	2	fvexi	⊢ 𝐵 ∈ V
11		resiexg	⊢ ( 𝐵 ∈ V → ( I ↾ 𝐵 ) ∈ V )
12	10 11	ax-mp	⊢ ( I ↾ 𝐵 ) ∈ V
13	10 10	xpex	⊢ ( 𝐵 × 𝐵 ) ∈ V
14	13	mptex	⊢ ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ∈ V
15	12 14	op2nd	⊢ ( 2nd ‘ ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ) = ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) )
16	9 15	eqtrdi	⊢ ( 𝜑 → ( 2nd ‘ 𝐼 ) = ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) )
17		simpr	⊢ ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ )
18	17	fveq2d	⊢ ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
19		df-ov	⊢ ( 𝑋 𝐻 𝑌 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
20	18 19	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( 𝐻 ‘ 𝑧 ) = ( 𝑋 𝐻 𝑌 ) )
21	20	reseq2d	⊢ ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( I ↾ ( 𝐻 ‘ 𝑧 ) ) = ( I ↾ ( 𝑋 𝐻 𝑌 ) ) )
22	5 6	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
23		ovex	⊢ ( 𝑋 𝐻 𝑌 ) ∈ V
24		resiexg	⊢ ( ( 𝑋 𝐻 𝑌 ) ∈ V → ( I ↾ ( 𝑋 𝐻 𝑌 ) ) ∈ V )
25	23 24	mp1i	⊢ ( 𝜑 → ( I ↾ ( 𝑋 𝐻 𝑌 ) ) ∈ V )
26	16 21 22 25	fvmptd	⊢ ( 𝜑 → ( ( 2nd ‘ 𝐼 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( I ↾ ( 𝑋 𝐻 𝑌 ) ) )
27	7 26	syl5eq	⊢ ( 𝜑 → ( 𝑋 ( 2nd ‘ 𝐼 ) 𝑌 ) = ( I ↾ ( 𝑋 𝐻 𝑌 ) ) )