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	No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
	thincmo.x	$$⊢\phi \to X\in B$$
	thincmo.y	$$⊢\phi \to Y\in B$$
	thincmo.b	$$⊢B={\mathrm{Base}}_C$$
	thincmo.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
Assertion	thincmoALT	$$⊢\phi \to {\exists }^{*}ff\in \left(XHY\right)$$

Proof

Step	Hyp	Ref	Expression
1		thincmo.c	Could not format ( ph -> C e. ThinCat ) : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
2		thincmo.x	$$⊢\phi \to X\in B$$
3		thincmo.y	$$⊢\phi \to Y\in B$$
4		thincmo.b	$$⊢B={\mathrm{Base}}_C$$
5		thincmo.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
6	4 5	isthinc	Could not format ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) ) : No typesetting found for |- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) ) with typecode |-
7	6	simprbi	Could not format ( C e. ThinCat -> A. x e. B A. y e. B E* f f e. ( x H y ) ) : No typesetting found for |- ( C e. ThinCat -> A. x e. B A. y e. B E* f f e. ( x H y ) ) with typecode |-
8	1 7	syl	$$⊢\phi \to \forall x\in B\forall y\in B{\exists }^{*}ff\in \left(xHy\right)$$
9		oveq12	$$⊢\left(x=X\wedge y=Y\right)\to xHy=XHY$$
10	9	eleq2d	$$⊢\left(x=X\wedge y=Y\right)\to \left(f\in \left(xHy\right)\leftrightarrow f\in \left(XHY\right)\right)$$
11	10	mobidv	$$⊢\left(x=X\wedge y=Y\right)\to \left({\exists }^{*}ff\in \left(xHy\right)\leftrightarrow {\exists }^{*}ff\in \left(XHY\right)\right)$$
12	11	rspc2gv	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall x\in B\forall y\in B{\exists }^{*}ff\in \left(xHy\right)\to {\exists }^{*}ff\in \left(XHY\right)\right)$$
13	2 3 12	syl2anc	$$⊢\phi \to \left(\forall x\in B\forall y\in B{\exists }^{*}ff\in \left(xHy\right)\to {\exists }^{*}ff\in \left(XHY\right)\right)$$
14	8 13	mpd	$$⊢\phi \to {\exists }^{*}ff\in \left(XHY\right)$$