Theorem catcrcl2

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)$$
	catcrcl2.b	$$⊢B={\mathrm{Base}}_C$$
Assertion	catcrcl2	$$⊢\phi \to \left(X\in B\wedge Y\in B\right)$$

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		catcrcl2.b	$$⊢B={\mathrm{Base}}_C$$
5	1 2 3	catcrcl	$$⊢\phi \to U\in \mathrm{V}$$
6	1 4 5 2	catchomfval	$$⊢\phi \to H=\left(x\in B,y\in B⟼x\mathrm{Func}y\right)$$
7	6	oveqd	$$⊢\phi \to XHY=X\left(x\in B,y\in B⟼x\mathrm{Func}y\right)Y$$
8	3 7	eleqtrd	$$⊢\phi \to F\in \left(X\left(x\in B,y\in B⟼x\mathrm{Func}y\right)Y\right)$$
9		eqid	$$⊢\left(x\in B,y\in B⟼x\mathrm{Func}y\right)=\left(x\in B,y\in B⟼x\mathrm{Func}y\right)$$
10	9	elmpocl	$$⊢F\in \left(X\left(x\in B,y\in B⟼x\mathrm{Func}y\right)Y\right)\to \left(X\in B\wedge Y\in B\right)$$
11	8 10	syl	$$⊢\phi \to \left(X\in B\wedge Y\in B\right)$$