Metamath Proof Explorer


Theorem catrid

Description: Right identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses catidcl.b 𝐵 = ( Base ‘ 𝐶 )
catidcl.h 𝐻 = ( Hom ‘ 𝐶 )
catidcl.i 1 = ( Id ‘ 𝐶 )
catidcl.c ( 𝜑𝐶 ∈ Cat )
catidcl.x ( 𝜑𝑋𝐵 )
catlid.o · = ( comp ‘ 𝐶 )
catlid.y ( 𝜑𝑌𝐵 )
catlid.f ( 𝜑𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion catrid ( 𝜑 → ( 𝐹 ( ⟨ 𝑋 , 𝑋· 𝑌 ) ( 1𝑋 ) ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 catidcl.b 𝐵 = ( Base ‘ 𝐶 )
2 catidcl.h 𝐻 = ( Hom ‘ 𝐶 )
3 catidcl.i 1 = ( Id ‘ 𝐶 )
4 catidcl.c ( 𝜑𝐶 ∈ Cat )
5 catidcl.x ( 𝜑𝑋𝐵 )
6 catlid.o · = ( comp ‘ 𝐶 )
7 catlid.y ( 𝜑𝑌𝐵 )
8 catlid.f ( 𝜑𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
9 oveq1 ( 𝑓 = 𝐹 → ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑌 ) ( 1𝑋 ) ) = ( 𝐹 ( ⟨ 𝑋 , 𝑋· 𝑌 ) ( 1𝑋 ) ) )
10 id ( 𝑓 = 𝐹𝑓 = 𝐹 )
11 9 10 eqeq12d ( 𝑓 = 𝐹 → ( ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑌 ) ( 1𝑋 ) ) = 𝑓 ↔ ( 𝐹 ( ⟨ 𝑋 , 𝑋· 𝑌 ) ( 1𝑋 ) ) = 𝐹 ) )
12 oveq2 ( 𝑦 = 𝑌 → ( 𝑋 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
13 oveq2 ( 𝑦 = 𝑌 → ( ⟨ 𝑋 , 𝑋· 𝑦 ) = ( ⟨ 𝑋 , 𝑋· 𝑌 ) )
14 13 oveqd ( 𝑦 = 𝑌 → ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) ( 1𝑋 ) ) = ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑌 ) ( 1𝑋 ) ) )
15 14 eqeq1d ( 𝑦 = 𝑌 → ( ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) ( 1𝑋 ) ) = 𝑓 ↔ ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑌 ) ( 1𝑋 ) ) = 𝑓 ) )
16 12 15 raleqbidv ( 𝑦 = 𝑌 → ( ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) ( 1𝑋 ) ) = 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑌 ) ( 1𝑋 ) ) = 𝑓 ) )
17 simpr ( ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) → ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 )
18 17 ralimi ( ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) → ∀ 𝑦𝐵𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 )
19 18 a1i ( 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) → ( ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) → ∀ 𝑦𝐵𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) )
20 19 ss2rabi { 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∣ ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) } ⊆ { 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∣ ∀ 𝑦𝐵𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 }
21 1 2 6 4 3 5 cidval ( 𝜑 → ( 1𝑋 ) = ( 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) ) )
22 1 2 6 4 5 catideu ( 𝜑 → ∃! 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) )
23 riotacl2 ( ∃! 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) → ( 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) ) ∈ { 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∣ ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) } )
24 22 23 syl ( 𝜑 → ( 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) ) ∈ { 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∣ ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) } )
25 21 24 eqeltrd ( 𝜑 → ( 1𝑋 ) ∈ { 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∣ ∀ 𝑦𝐵 ( ∀ 𝑓 ∈ ( 𝑦 𝐻 𝑋 ) ( 𝑔 ( ⟨ 𝑦 , 𝑋· 𝑋 ) 𝑓 ) = 𝑓 ∧ ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ) } )
26 20 25 sselid ( 𝜑 → ( 1𝑋 ) ∈ { 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∣ ∀ 𝑦𝐵𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 } )
27 oveq2 ( 𝑔 = ( 1𝑋 ) → ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) ( 1𝑋 ) ) )
28 27 eqeq1d ( 𝑔 = ( 1𝑋 ) → ( ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ↔ ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) ( 1𝑋 ) ) = 𝑓 ) )
29 28 2ralbidv ( 𝑔 = ( 1𝑋 ) → ( ∀ 𝑦𝐵𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 ↔ ∀ 𝑦𝐵𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) ( 1𝑋 ) ) = 𝑓 ) )
30 29 elrab ( ( 1𝑋 ) ∈ { 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∣ ∀ 𝑦𝐵𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 } ↔ ( ( 1𝑋 ) ∈ ( 𝑋 𝐻 𝑋 ) ∧ ∀ 𝑦𝐵𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) ( 1𝑋 ) ) = 𝑓 ) )
31 30 simprbi ( ( 1𝑋 ) ∈ { 𝑔 ∈ ( 𝑋 𝐻 𝑋 ) ∣ ∀ 𝑦𝐵𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) 𝑔 ) = 𝑓 } → ∀ 𝑦𝐵𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) ( 1𝑋 ) ) = 𝑓 )
32 26 31 syl ( 𝜑 → ∀ 𝑦𝐵𝑓 ∈ ( 𝑋 𝐻 𝑦 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑦 ) ( 1𝑋 ) ) = 𝑓 )
33 16 32 7 rspcdva ( 𝜑 → ∀ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ( 𝑓 ( ⟨ 𝑋 , 𝑋· 𝑌 ) ( 1𝑋 ) ) = 𝑓 )
34 11 33 8 rspcdva ( 𝜑 → ( 𝐹 ( ⟨ 𝑋 , 𝑋· 𝑌 ) ( 1𝑋 ) ) = 𝐹 )