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	|- ( 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 ) )