Theorem initopropdlem

Description: Lemma for initopropd . (Contributed by Zhi Wang, 26-Oct-2025)

	Ref	Expression
Hypotheses	initopropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
	initopropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
	initopropdlem.1	$$⊢\phi \to \neg C\in \mathrm{V}$$
Assertion	initopropdlem	$$⊢\phi \to \mathrm{InitO}\left(C\right)=\mathrm{InitO}\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		initopropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
2		initopropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
3		initopropdlem.1	$$⊢\phi \to \neg C\in \mathrm{V}$$
4		initofn	$$⊢\mathrm{InitO}Fn\mathrm{Cat}$$
5		ssv	$$⊢\mathrm{Cat}\subseteq \mathrm{V}$$
6		simpr	$$⊢\left(\phi \wedge D\in \mathrm{Cat}\right)\to D\in \mathrm{Cat}$$
7		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
8		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
9	6 7 8	initoval	$$⊢\left(\phi \wedge D\in \mathrm{Cat}\right)\to \mathrm{InitO}\left(D\right)=\left\{a\in {\mathrm{Base}}_D|\forall b\in {\mathrm{Base}}_D\exists !hh\in \left(a\mathrm{Hom}\left(D\right)b\right)\right\}$$
10		fvprc	$$⊢\neg C\in \mathrm{V}\to {\mathrm{Hom}}_{𝑓}\left(C\right)=\varnothing$$
11	3 10	syl	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)=\varnothing$$
12	1 11	eqtr3d	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(D\right)=\varnothing$$
13		homf0	$$⊢{\mathrm{Base}}_D=\varnothing \leftrightarrow {\mathrm{Hom}}_{𝑓}\left(D\right)=\varnothing$$
14	12 13	sylibr	$$⊢\phi \to {\mathrm{Base}}_D=\varnothing$$
15	14	rabeqdv	$$⊢\phi \to \left\{a\in {\mathrm{Base}}_D|\forall b\in {\mathrm{Base}}_D\exists !hh\in \left(a\mathrm{Hom}\left(D\right)b\right)\right\}=\left\{a\in \varnothing |\forall b\in {\mathrm{Base}}_D\exists !hh\in \left(a\mathrm{Hom}\left(D\right)b\right)\right\}$$
16		rab0	$$⊢\left\{a\in \varnothing |\forall b\in {\mathrm{Base}}_D\exists !hh\in \left(a\mathrm{Hom}\left(D\right)b\right)\right\}=\varnothing$$
17	15 16	eqtrdi	$$⊢\phi \to \left\{a\in {\mathrm{Base}}_D|\forall b\in {\mathrm{Base}}_D\exists !hh\in \left(a\mathrm{Hom}\left(D\right)b\right)\right\}=\varnothing$$
18	17	adantr	$$⊢\left(\phi \wedge D\in \mathrm{Cat}\right)\to \left\{a\in {\mathrm{Base}}_D|\forall b\in {\mathrm{Base}}_D\exists !hh\in \left(a\mathrm{Hom}\left(D\right)b\right)\right\}=\varnothing$$
19	9 18	eqtrd	$$⊢\left(\phi \wedge D\in \mathrm{Cat}\right)\to \mathrm{InitO}\left(D\right)=\varnothing$$
20	4 3 5 19	initopropdlemlem	$$⊢\phi \to \mathrm{InitO}\left(C\right)=\mathrm{InitO}\left(D\right)$$