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

Metamath Proof Explorer

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

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 catcrcl2.b ⊢ B = Base C
5 1 2 3 catcrcl ⊢ φ → U ∈ V
6 1 4 5 2 catchomfval ⊢ φ → H = x ∈ B , y ∈ B ⟼ x Func y
7 6 oveqd ⊢ φ → X H Y = X x ∈ B , y ∈ B ⟼ x Func y Y
8 3 7 eleqtrd ⊢ φ → F ∈ X x ∈ B , y ∈ B ⟼ x Func y Y
9 eqid ⊢ x ∈ B , y ∈ B ⟼ x Func y = x ∈ B , y ∈ B ⟼ x Func y
10 9 elmpocl ⊢ F ∈ X x ∈ B , y ∈ B ⟼ x Func y Y → X ∈ B ∧ Y ∈ B
11 8 10 syl ⊢ φ → X ∈ B ∧ Y ∈ B