Theorem xpcid

Description: The identity morphism in the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	xpccat.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
	xpccat.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	xpccat.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	xpccat.x	⊢ 𝑋 = ( Base ‘ 𝐶 )
	xpccat.y	⊢ 𝑌 = ( Base ‘ 𝐷 )
	xpccat.i	⊢ 𝐼 = ( Id ‘ 𝐶 )
	xpccat.j	⊢ 𝐽 = ( Id ‘ 𝐷 )
	xpcid.1	⊢ 1 = ( Id ‘ 𝑇 )
	xpcid.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
	xpcid.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
Assertion	xpcid	⊢ ( 𝜑 → ( 1 ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = ⟨ ( 𝐼 ‘ 𝑅 ) , ( 𝐽 ‘ 𝑆 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		xpccat.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
2		xpccat.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		xpccat.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
4		xpccat.x	⊢ 𝑋 = ( Base ‘ 𝐶 )
5		xpccat.y	⊢ 𝑌 = ( Base ‘ 𝐷 )
6		xpccat.i	⊢ 𝐼 = ( Id ‘ 𝐶 )
7		xpccat.j	⊢ 𝐽 = ( Id ‘ 𝐷 )
8		xpcid.1	⊢ 1 = ( Id ‘ 𝑇 )
9		xpcid.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
10		xpcid.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
11		df-ov	⊢ ( 𝑅 1 𝑆 ) = ( 1 ‘ ⟨ 𝑅 , 𝑆 ⟩ )
12	1 2 3 4 5 6 7	xpccatid	⊢ ( 𝜑 → ( 𝑇 ∈ Cat ∧ ( Id ‘ 𝑇 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ ( 𝐼 ‘ 𝑥 ) , ( 𝐽 ‘ 𝑦 ) ⟩ ) ) )
13	12	simprd	⊢ ( 𝜑 → ( Id ‘ 𝑇 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ ( 𝐼 ‘ 𝑥 ) , ( 𝐽 ‘ 𝑦 ) ⟩ ) )
14	8 13	syl5eq	⊢ ( 𝜑 → 1 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ ( 𝐼 ‘ 𝑥 ) , ( 𝐽 ‘ 𝑦 ) ⟩ ) )
15		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → 𝑥 = 𝑅 )
16	15	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑅 ) )
17		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → 𝑦 = 𝑆 )
18	17	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → ( 𝐽 ‘ 𝑦 ) = ( 𝐽 ‘ 𝑆 ) )
19	16 18	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑅 ∧ 𝑦 = 𝑆 ) ) → ⟨ ( 𝐼 ‘ 𝑥 ) , ( 𝐽 ‘ 𝑦 ) ⟩ = ⟨ ( 𝐼 ‘ 𝑅 ) , ( 𝐽 ‘ 𝑆 ) ⟩ )
20		opex	⊢ ⟨ ( 𝐼 ‘ 𝑅 ) , ( 𝐽 ‘ 𝑆 ) ⟩ ∈ V
21	20	a1i	⊢ ( 𝜑 → ⟨ ( 𝐼 ‘ 𝑅 ) , ( 𝐽 ‘ 𝑆 ) ⟩ ∈ V )
22	14 19 9 10 21	ovmpod	⊢ ( 𝜑 → ( 𝑅 1 𝑆 ) = ⟨ ( 𝐼 ‘ 𝑅 ) , ( 𝐽 ‘ 𝑆 ) ⟩ )
23	11 22	syl5eqr	⊢ ( 𝜑 → ( 1 ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = ⟨ ( 𝐼 ‘ 𝑅 ) , ( 𝐽 ‘ 𝑆 ) ⟩ )