Metamath Proof Explorer


Theorem thincmoALT

Description: Alternate proof for thincmo . (Contributed by Zhi Wang, 21-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses thincmo.c φ C ThinCat
thincmo.x φ X B
thincmo.y φ Y B
thincmo.b B = Base C
thincmo.h H = Hom C
Assertion thincmoALT φ * f f X H Y

Proof

Step Hyp Ref Expression
1 thincmo.c φ C ThinCat
2 thincmo.x φ X B
3 thincmo.y φ Y B
4 thincmo.b B = Base C
5 thincmo.h H = Hom C
6 4 5 isthinc C ThinCat C Cat x B y B * f f x H y
7 6 simprbi C ThinCat x B y B * f f x H y
8 1 7 syl φ x B y B * f f x H y
9 oveq12 x = X y = Y x H y = X H Y
10 9 eleq2d x = X y = Y f x H y f X H Y
11 10 mobidv x = X y = Y * f f x H y * f f X H Y
12 11 rspc2gv X B Y B x B y B * f f x H y * f f X H Y
13 2 3 12 syl2anc φ x B y B * f f x H y * f f X H Y
14 8 13 mpd φ * f f X H Y