Metamath Proof Explorer


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 eqtrid ( 𝜑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 eqtr3id ( 𝜑 → ( 1 ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = ⟨ ( 𝐼𝑅 ) , ( 𝐽𝑆 ) ⟩ )