This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )