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 B = Base C
catidcl.h H = Hom C
catidcl.i 1 ˙ = Id C
catidcl.c φ C Cat
catidcl.x φ X B
catlid.o · ˙ = comp C
catlid.y φ Y B
catlid.f φ F X H Y
Assertion catrid φ F X X · ˙ Y 1 ˙ X = F

Proof

Step Hyp Ref Expression
1 catidcl.b B = Base C
2 catidcl.h H = Hom C
3 catidcl.i 1 ˙ = Id C
4 catidcl.c φ C Cat
5 catidcl.x φ X B
6 catlid.o · ˙ = comp C
7 catlid.y φ Y B
8 catlid.f φ F X H Y
9 oveq1 f = F f X X · ˙ Y 1 ˙ X = F X X · ˙ Y 1 ˙ X
10 id f = F f = F
11 9 10 eqeq12d f = F f X X · ˙ Y 1 ˙ X = f F X X · ˙ Y 1 ˙ X = F
12 oveq2 y = Y X H y = X H Y
13 oveq2 y = Y X X · ˙ y = X X · ˙ Y
14 13 oveqd y = Y f X X · ˙ y 1 ˙ X = f X X · ˙ Y 1 ˙ X
15 14 eqeq1d y = Y f X X · ˙ y 1 ˙ X = f f X X · ˙ Y 1 ˙ X = f
16 12 15 raleqbidv y = Y f X H y f X X · ˙ y 1 ˙ X = f f X H Y f X X · ˙ Y 1 ˙ X = f
17 simpr f y H X g y X · ˙ X f = f f X H y f X X · ˙ y g = f f X H y f X X · ˙ y g = f
18 17 ralimi y B f y H X g y X · ˙ X f = f f X H y f X X · ˙ y g = f y B f X H y f X X · ˙ y g = f
19 18 a1i g X H X y B f y H X g y X · ˙ X f = f f X H y f X X · ˙ y g = f y B f X H y f X X · ˙ y g = f
20 19 ss2rabi g X H X | y B f y H X g y X · ˙ X f = f f X H y f X X · ˙ y g = f g X H X | y B f X H y f X X · ˙ y g = f
21 1 2 6 4 3 5 cidval φ 1 ˙ X = ι g X H X | y B f y H X g y X · ˙ X f = f f X H y f X X · ˙ y g = f
22 1 2 6 4 5 catideu φ ∃! g X H X y B f y H X g y X · ˙ X f = f f X H y f X X · ˙ y g = f
23 riotacl2 ∃! g X H X y B f y H X g y X · ˙ X f = f f X H y f X X · ˙ y g = f ι g X H X | y B f y H X g y X · ˙ X f = f f X H y f X X · ˙ y g = f g X H X | y B f y H X g y X · ˙ X f = f f X H y f X X · ˙ y g = f
24 22 23 syl φ ι g X H X | y B f y H X g y X · ˙ X f = f f X H y f X X · ˙ y g = f g X H X | y B f y H X g y X · ˙ X f = f f X H y f X X · ˙ y g = f
25 21 24 eqeltrd φ 1 ˙ X g X H X | y B f y H X g y X · ˙ X f = f f X H y f X X · ˙ y g = f
26 20 25 sseldi φ 1 ˙ X g X H X | y B f X H y f X X · ˙ y g = f
27 oveq2 g = 1 ˙ X f X X · ˙ y g = f X X · ˙ y 1 ˙ X
28 27 eqeq1d g = 1 ˙ X f X X · ˙ y g = f f X X · ˙ y 1 ˙ X = f
29 28 2ralbidv g = 1 ˙ X y B f X H y f X X · ˙ y g = f y B f X H y f X X · ˙ y 1 ˙ X = f
30 29 elrab 1 ˙ X g X H X | y B f X H y f X X · ˙ y g = f 1 ˙ X X H X y B f X H y f X X · ˙ y 1 ˙ X = f
31 30 simprbi 1 ˙ X g X H X | y B f X H y f X X · ˙ y g = f y B f X H y f X X · ˙ y 1 ˙ X = f
32 26 31 syl φ y B f X H y f X X · ˙ y 1 ˙ X = f
33 16 32 7 rspcdva φ f X H Y f X X · ˙ Y 1 ˙ X = f
34 11 33 8 rspcdva φ F X X · ˙ Y 1 ˙ X = F