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

Proof

Step	Hyp	Ref	Expression
1		catcrcl.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2		catcrcl.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		catcrcl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
4		elfvne0	⊢ ( 𝐹 ∈ ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) → 𝐻 ≠ ∅ )
5		df-ov	⊢ ( 𝑋 𝐻 𝑌 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
6	4 5	eleq2s	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐻 ≠ ∅ )
7		fvprc	⊢ ( ¬ 𝑈 ∈ V → ( CatCat ‘ 𝑈 ) = ∅ )
8	1 7	eqtrid	⊢ ( ¬ 𝑈 ∈ V → 𝐶 = ∅ )
9		fveq2	⊢ ( 𝐶 = ∅ → ( Hom ‘ 𝐶 ) = ( Hom ‘ ∅ ) )
10		homid	⊢ Hom = Slot ( Hom ‘ ndx )
11	10	str0	⊢ ∅ = ( Hom ‘ ∅ )
12	9 2 11	3eqtr4g	⊢ ( 𝐶 = ∅ → 𝐻 = ∅ )
13	8 12	syl	⊢ ( ¬ 𝑈 ∈ V → 𝐻 = ∅ )
14	13	necon1ai	⊢ ( 𝐻 ≠ ∅ → 𝑈 ∈ V )
15	3 6 14	3syl	⊢ ( 𝜑 → 𝑈 ∈ V )