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 ⊢ C = CatCat ⁡ U
catcrcl.h ⊢ H = Hom ⁡ C
catcrcl.f ⊢ φ → F ∈ X H Y
Assertion catcrcl ⊢ φ → U ∈ V

Proof

Step Hyp Ref Expression
1 catcrcl.c ⊢ C = CatCat ⁡ U
2 catcrcl.h ⊢ H = Hom ⁡ C
3 catcrcl.f ⊢ φ → F ∈ X H Y
4 elfvne0 ⊢ F ∈ H ⁡ X Y → H ≠ ∅
5 df-ov ⊢ X H Y = H ⁡ X Y
6 4 5 eleq2s ⊢ F ∈ X H Y → H ≠ ∅
7 fvprc ⊢ ¬ U ∈ V → CatCat ⁡ U = ∅
8 1 7 eqtrid ⊢ ¬ U ∈ V → C = ∅
9 fveq2 ⊢ C = ∅ → Hom ⁡ C = Hom ⁡ ∅
10 homid ⊢ Hom = Slot Hom ⁡ ndx
11 10 str0 ⊢ ∅ = Hom ⁡ ∅
12 9 2 11 3eqtr4g ⊢ C = ∅ → H = ∅
13 8 12 syl ⊢ ¬ U ∈ V → H = ∅
14 13 necon1ai ⊢ H ≠ ∅ → U ∈ V
15 3 6 14 3syl ⊢ φ → U ∈ V