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	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
	catcrcl.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	catcrcl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
	catcrcl2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	catcrcl2	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		catcrcl.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2		catcrcl.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		catcrcl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
4		catcrcl2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
5	1 2 3	catcrcl	⊢ ( 𝜑 → 𝑈 ∈ V )
6	1 4 5 2	catchomfval	⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) )
7	6	oveqd	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) 𝑌 ) )
8	3 7	eleqtrd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) 𝑌 ) )
9		eqid	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) )
10	9	elmpocl	⊢ ( 𝐹 ∈ ( 𝑋 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 Func 𝑦 ) ) 𝑌 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
11	8 10	syl	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )