This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem thincmoALT

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

Ref Expression
Hypotheses thincmo.c 
|- ( ph -> C e. ThinCat )
thincmo.x 
|- ( ph -> X e. B )
thincmo.y 
|- ( ph -> Y e. B )
thincmo.b 
|- B = ( Base ` C )
thincmo.h 
|- H = ( Hom ` C )
Assertion thincmoALT 
|- ( ph -> E* f f e. ( X H Y ) )

Proof

Step Hyp Ref Expression
1 thincmo.c 
 |-  ( ph -> C e. ThinCat )
2 thincmo.x 
 |-  ( ph -> X e. B )
3 thincmo.y 
 |-  ( ph -> Y e. B )
4 thincmo.b 
 |-  B = ( Base ` C )
5 thincmo.h 
 |-  H = ( Hom ` C )
6 4 5 isthinc 
 |-  ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) )
7 6 simprbi 
 |-  ( C e. ThinCat -> A. x e. B A. y e. B E* f f e. ( x H y ) )
8 1 7 syl 
 |-  ( ph -> A. x e. B A. y e. B E* f f e. ( x H y ) )
9 oveq12 
 |-  ( ( x = X /\ y = Y ) -> ( x H y ) = ( X H Y ) )
10 9 eleq2d 
 |-  ( ( x = X /\ y = Y ) -> ( f e. ( x H y ) <-> f e. ( X H Y ) ) )
11 10 mobidv 
 |-  ( ( x = X /\ y = Y ) -> ( E* f f e. ( x H y ) <-> E* f f e. ( X H Y ) ) )
12 11 rspc2gv 
 |-  ( ( X e. B /\ Y e. B ) -> ( A. x e. B A. y e. B E* f f e. ( x H y ) -> E* f f e. ( X H Y ) ) )
13 2 3 12 syl2anc 
 |-  ( ph -> ( A. x e. B A. y e. B E* f f e. ( x H y ) -> E* f f e. ( X H Y ) ) )
14 8 13 mpd 
 |-  ( ph -> E* f f e. ( X H Y ) )