Theorem homf0

Description: The base is empty iff the functionalized Hom-set operation is empty. (Contributed by Zhi Wang, 23-Oct-2025)

	Ref	Expression
Assertion	homf0	$$⊢{\mathrm{Base}}_C=\varnothing \leftrightarrow {\mathrm{Hom}}_{𝑓}\left(C\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
2		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
3		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
4	1 2 3	homffval	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)=\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼x\mathrm{Hom}\left(C\right)y\right)$$
5		0mpo0	$$⊢\left({\mathrm{Base}}_C=\varnothing \vee {\mathrm{Base}}_C=\varnothing \right)\to \left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼x\mathrm{Hom}\left(C\right)y\right)=\varnothing$$
6	5	orcs	$$⊢{\mathrm{Base}}_C=\varnothing \to \left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼x\mathrm{Hom}\left(C\right)y\right)=\varnothing$$
7	4 6	eqtrid	$$⊢{\mathrm{Base}}_C=\varnothing \to {\mathrm{Hom}}_{𝑓}\left(C\right)=\varnothing$$
8	1 2	homffn	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
9		f0bi	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right):\varnothing ⟶\varnothing \leftrightarrow {\mathrm{Hom}}_{𝑓}\left(C\right)=\varnothing$$
10		ffn	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right):\varnothing ⟶\varnothing \to {\mathrm{Hom}}_{𝑓}\left(C\right)Fn\varnothing$$
11	9 10	sylbir	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)=\varnothing \to {\mathrm{Hom}}_{𝑓}\left(C\right)Fn\varnothing$$
12		fndmu	$$⊢\left({\mathrm{Hom}}_{𝑓}\left(C\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\wedge {\mathrm{Hom}}_{𝑓}\left(C\right)Fn\varnothing \right)\to {\mathrm{Base}}_C\times {\mathrm{Base}}_C=\varnothing$$
13	8 11 12	sylancr	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)=\varnothing \to {\mathrm{Base}}_C\times {\mathrm{Base}}_C=\varnothing$$
14		xpeq0	$$⊢{\mathrm{Base}}_C\times {\mathrm{Base}}_C=\varnothing \leftrightarrow \left({\mathrm{Base}}_C=\varnothing \vee {\mathrm{Base}}_C=\varnothing \right)$$
15		pm4.25	$$⊢{\mathrm{Base}}_C=\varnothing \leftrightarrow \left({\mathrm{Base}}_C=\varnothing \vee {\mathrm{Base}}_C=\varnothing \right)$$
16	14 15	bitr4i	$$⊢{\mathrm{Base}}_C\times {\mathrm{Base}}_C=\varnothing \leftrightarrow {\mathrm{Base}}_C=\varnothing$$
17	13 16	sylib	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)=\varnothing \to {\mathrm{Base}}_C=\varnothing$$
18	7 17	impbii	$$⊢{\mathrm{Base}}_C=\varnothing \leftrightarrow {\mathrm{Hom}}_{𝑓}\left(C\right)=\varnothing$$