Theorem fullthinc2

Description: A full functor to a thin category maps empty hom-sets to empty hom-sets. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Hypotheses	fullthinc.b	$$⊢B={\mathrm{Base}}_C$$
	fullthinc.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
	fullthinc.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	fullthinc.d	No typesetting found for |- ( ph -> D e. ThinCat ) with typecode |-
	fullthinc2.f	$$⊢\phi \to F\left(C\mathrm{Full}D\right)G$$
	fullthinc2.x	$$⊢\phi \to X\in B$$
	fullthinc2.y	$$⊢\phi \to Y\in B$$
Assertion	fullthinc2	$$⊢\phi \to \left(XHY=\varnothing \leftrightarrow F\left(X\right)JF\left(Y\right)=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		fullthinc.b	$$⊢B={\mathrm{Base}}_C$$
2		fullthinc.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
3		fullthinc.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
4		fullthinc.d	Could not format ( ph -> D e. ThinCat ) : No typesetting found for |- ( ph -> D e. ThinCat ) with typecode |-
5		fullthinc2.f	$$⊢\phi \to F\left(C\mathrm{Full}D\right)G$$
6		fullthinc2.x	$$⊢\phi \to X\in B$$
7		fullthinc2.y	$$⊢\phi \to Y\in B$$
8		fullfunc	$$⊢C\mathrm{Full}D\subseteq C\mathrm{Func}D$$
9	8	ssbri	$$⊢F\left(C\mathrm{Full}D\right)G\to F\left(C\mathrm{Func}D\right)G$$
10	5 9	syl	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
11	1 2 3 4 10	fullthinc	$$⊢\phi \to \left(F\left(C\mathrm{Full}D\right)G\leftrightarrow \forall x\in B\forall y\in B\left(xHy=\varnothing \to F\left(x\right)JF\left(y\right)=\varnothing \right)\right)$$
12	5 11	mpbid	$$⊢\phi \to \forall x\in B\forall y\in B\left(xHy=\varnothing \to F\left(x\right)JF\left(y\right)=\varnothing \right)$$
13		oveq12	$$⊢\left(x=X\wedge y=Y\right)\to xHy=XHY$$
14	13	eqeq1d	$$⊢\left(x=X\wedge y=Y\right)\to \left(xHy=\varnothing \leftrightarrow XHY=\varnothing \right)$$
15		simpl	$$⊢\left(x=X\wedge y=Y\right)\to x=X$$
16	15	fveq2d	$$⊢\left(x=X\wedge y=Y\right)\to F\left(x\right)=F\left(X\right)$$
17		simpr	$$⊢\left(x=X\wedge y=Y\right)\to y=Y$$
18	17	fveq2d	$$⊢\left(x=X\wedge y=Y\right)\to F\left(y\right)=F\left(Y\right)$$
19	16 18	oveq12d	$$⊢\left(x=X\wedge y=Y\right)\to F\left(x\right)JF\left(y\right)=F\left(X\right)JF\left(Y\right)$$
20	19	eqeq1d	$$⊢\left(x=X\wedge y=Y\right)\to \left(F\left(x\right)JF\left(y\right)=\varnothing \leftrightarrow F\left(X\right)JF\left(Y\right)=\varnothing \right)$$
21	14 20	imbi12d	$$⊢\left(x=X\wedge y=Y\right)\to \left(\left(xHy=\varnothing \to F\left(x\right)JF\left(y\right)=\varnothing \right)\leftrightarrow \left(XHY=\varnothing \to F\left(X\right)JF\left(Y\right)=\varnothing \right)\right)$$
22	21	rspc2gv	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall x\in B\forall y\in B\left(xHy=\varnothing \to F\left(x\right)JF\left(y\right)=\varnothing \right)\to \left(XHY=\varnothing \to F\left(X\right)JF\left(Y\right)=\varnothing \right)\right)$$
23	22	imp	$$⊢\left(\left(X\in B\wedge Y\in B\right)\wedge \forall x\in B\forall y\in B\left(xHy=\varnothing \to F\left(x\right)JF\left(y\right)=\varnothing \right)\right)\to \left(XHY=\varnothing \to F\left(X\right)JF\left(Y\right)=\varnothing \right)$$
24	6 7 12 23	syl21anc	$$⊢\phi \to \left(XHY=\varnothing \to F\left(X\right)JF\left(Y\right)=\varnothing \right)$$
25	1 3 2 10 6 7	funcf2	$$⊢\phi \to \left(XGY\right):XHY⟶F\left(X\right)JF\left(Y\right)$$
26	25	f002	$$⊢\phi \to \left(F\left(X\right)JF\left(Y\right)=\varnothing \to XHY=\varnothing \right)$$
27	24 26	impbid	$$⊢\phi \to \left(XHY=\varnothing \leftrightarrow F\left(X\right)JF\left(Y\right)=\varnothing \right)$$