Theorem catcrcl

Description: Reverse closure for the category of categories (in a universe) (Contributed by Zhi Wang, 14-Nov-2025)

	Ref	Expression
Hypotheses	catcrcl.c	$$⊢C=\mathrm{CatCat}\left(U\right)$$
	catcrcl.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	catcrcl.f	$$⊢\phi \to F\in \left(XHY\right)$$
Assertion	catcrcl	$$⊢\phi \to U\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		catcrcl.c	$$⊢C=\mathrm{CatCat}\left(U\right)$$
2		catcrcl.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
3		catcrcl.f	$$⊢\phi \to F\in \left(XHY\right)$$
4		elfvne0	$$⊢F\in H\left(⟨X,Y⟩\right)\to H\ne \varnothing$$
5		df-ov	$$⊢XHY=H\left(⟨X,Y⟩\right)$$
6	4 5	eleq2s	$$⊢F\in \left(XHY\right)\to H\ne \varnothing$$
7		fvprc	$$⊢\neg U\in \mathrm{V}\to \mathrm{CatCat}\left(U\right)=\varnothing$$
8	1 7	eqtrid	$$⊢\neg U\in \mathrm{V}\to C=\varnothing$$
9		fveq2	$$⊢C=\varnothing \to \mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(\varnothing \right)$$
10		homid	$$⊢\mathrm{Hom}=\mathrm{Slot}\mathrm{Hom}\left(\mathrm{ndx}\right)$$
11	10	str0	$$⊢\varnothing =\mathrm{Hom}\left(\varnothing \right)$$
12	9 2 11	3eqtr4g	$$⊢C=\varnothing \to H=\varnothing$$
13	8 12	syl	$$⊢\neg U\in \mathrm{V}\to H=\varnothing$$
14	13	necon1ai	$$⊢H\ne \varnothing \to U\in \mathrm{V}$$
15	3 6 14	3syl	$$⊢\phi \to U\in \mathrm{V}$$