Metamath Proof Explorer

Theorem resccat

Description: A class C restricted by the hom-sets of another set E , whose base is a subset of the base of C and whose composition is compatible with C , is a category iff E is a category. Note that the compatibility condition "resccat.1" can be weakened by removing x e. S because f e. ( x J y ) implies these. (Contributed by Zhi Wang, 6-Nov-2025)

Ref Expression
Hypotheses resccat.d ⊢ D = C ↾ cat J
resccat.b ⊢ B = Base C
resccat.s ⊢ S = Base E
resccat.j ⊢ J = Hom 𝑓 ⁡ E
resccat.x ⊢ · ˙ = comp ⁡ C
resccat.xb ⊢ ∙ ˙ = comp ⁡ E
resccat.1 ⊢ φ ∧ x ∈ S ∧ y ∈ S ∧ z ∈ S ∧ f ∈ x J y ∧ g ∈ y J z → g x y · ˙ z f = g x y ∙ ˙ z f
resccat.e ⊢ φ → E ∈ V
resccat.ss ⊢ φ → S ⊆ B
Assertion resccat ⊢ φ → D ∈ Cat ↔ E ∈ Cat

Proof

Step Hyp Ref Expression
1 resccat.d ⊢ D = C ↾ cat J
2 resccat.b ⊢ B = Base C
3 resccat.s ⊢ S = Base E
4 resccat.j ⊢ J = Hom 𝑓 ⁡ E
5 resccat.x ⊢ · ˙ = comp ⁡ C
6 resccat.xb ⊢ ∙ ˙ = comp ⁡ E
7 resccat.1 ⊢ φ ∧ x ∈ S ∧ y ∈ S ∧ z ∈ S ∧ f ∈ x J y ∧ g ∈ y J z → g x y · ˙ z f = g x y ∙ ˙ z f
8 resccat.e ⊢ φ → E ∈ V
9 resccat.ss ⊢ φ → S ⊆ B
10 7 adantllr ⊢ φ ∧ C ∈ V ∧ x ∈ S ∧ y ∈ S ∧ z ∈ S ∧ f ∈ x J y ∧ g ∈ y J z → g x y · ˙ z f = g x y ∙ ˙ z f
11 8 adantr ⊢ φ ∧ C ∈ V → E ∈ V
12 9 adantr ⊢ φ ∧ C ∈ V → S ⊆ B
13 simpr ⊢ φ ∧ C ∈ V → C ∈ V
14 1 2 3 4 5 6 10 11 12 13 resccatlem ⊢ φ ∧ C ∈ V → D ∈ Cat ↔ E ∈ Cat
15 df-resc ⊢ ↾ cat = c ∈ V , h ∈ V ⟼ c ↾ 𝑠 dom ⁡ dom ⁡ h sSet Hom ⁡ ndx h
16 15 reldmmpo ⊢ Rel ⁡ dom ⁡ ↾ cat
17 16 ovprc1 ⊢ ¬ C ∈ V → C ↾ cat J = ∅
18 1 17 eqtrid ⊢ ¬ C ∈ V → D = ∅
19 0cat ⊢ ∅ ∈ Cat
20 18 19 eqeltrdi ⊢ ¬ C ∈ V → D ∈ Cat
21 20 adantl ⊢ φ ∧ ¬ C ∈ V → D ∈ Cat
22 fvprc ⊢ ¬ C ∈ V → Base C = ∅
23 2 22 eqtrid ⊢ ¬ C ∈ V → B = ∅
24 sseq0 ⊢ S ⊆ B ∧ B = ∅ → S = ∅
25 9 23 24 syl2an ⊢ φ ∧ ¬ C ∈ V → S = ∅
26 25 3 eqtr3di ⊢ φ ∧ ¬ C ∈ V → ∅ = Base E
27 0catg ⊢ E ∈ V ∧ ∅ = Base E → E ∈ Cat
28 8 26 27 syl2an2r ⊢ φ ∧ ¬ C ∈ V → E ∈ Cat
29 21 28 2thd ⊢ φ ∧ ¬ C ∈ V → D ∈ Cat ↔ E ∈ Cat
30 14 29 pm2.61dan ⊢ φ → D ∈ Cat ↔ E ∈ Cat