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	⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 )
	resccat.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	resccat.s	⊢ 𝑆 = ( Base ‘ 𝐸 )
	resccat.j	⊢ 𝐽 = ( Homf ‘ 𝐸 )
	resccat.x	⊢ · = ( comp ‘ 𝐶 )
	resccat.xb	⊢ ∙ = ( comp ‘ 𝐸 )
	resccat.1	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) )
	resccat.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
	resccat.ss	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
Assertion	resccat	⊢ ( 𝜑 → ( 𝐷 ∈ Cat ↔ 𝐸 ∈ Cat ) )

Proof

Step	Hyp	Ref	Expression
1		resccat.d	⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 )
2		resccat.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		resccat.s	⊢ 𝑆 = ( Base ‘ 𝐸 )
4		resccat.j	⊢ 𝐽 = ( Homf ‘ 𝐸 )
5		resccat.x	⊢ · = ( comp ‘ 𝐶 )
6		resccat.xb	⊢ ∙ = ( comp ‘ 𝐸 )
7		resccat.1	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) )
8		resccat.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
9		resccat.ss	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
10	7	adantllr	⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ V ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) )
11	8	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ V ) → 𝐸 ∈ 𝑉 )
12	9	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ V ) → 𝑆 ⊆ 𝐵 )
13		simpr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ V ) → 𝐶 ∈ V )
14	1 2 3 4 5 6 10 11 12 13	resccatlem	⊢ ( ( 𝜑 ∧ 𝐶 ∈ V ) → ( 𝐷 ∈ Cat ↔ 𝐸 ∈ Cat ) )
15		df-resc	⊢ ↾cat = ( 𝑐 ∈ V , ℎ ∈ V ↦ ( ( 𝑐 ↾s dom dom ℎ ) sSet ⟨ ( Hom ‘ ndx ) , ℎ ⟩ ) )
16	15	reldmmpo	⊢ Rel dom ↾cat
17	16	ovprc1	⊢ ( ¬ 𝐶 ∈ V → ( 𝐶 ↾cat 𝐽 ) = ∅ )
18	1 17	eqtrid	⊢ ( ¬ 𝐶 ∈ V → 𝐷 = ∅ )
19		0cat	⊢ ∅ ∈ Cat
20	18 19	eqeltrdi	⊢ ( ¬ 𝐶 ∈ V → 𝐷 ∈ Cat )
21	20	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → 𝐷 ∈ Cat )
22		fvprc	⊢ ( ¬ 𝐶 ∈ V → ( Base ‘ 𝐶 ) = ∅ )
23	2 22	eqtrid	⊢ ( ¬ 𝐶 ∈ V → 𝐵 = ∅ )
24		sseq0	⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝐵 = ∅ ) → 𝑆 = ∅ )
25	9 23 24	syl2an	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → 𝑆 = ∅ )
26	25 3	eqtr3di	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → ∅ = ( Base ‘ 𝐸 ) )
27		0catg	⊢ ( ( 𝐸 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐸 ) ) → 𝐸 ∈ Cat )
28	8 26 27	syl2an2r	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → 𝐸 ∈ Cat )
29	21 28	2thd	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → ( 𝐷 ∈ Cat ↔ 𝐸 ∈ Cat ) )
30	14 29	pm2.61dan	⊢ ( 𝜑 → ( 𝐷 ∈ Cat ↔ 𝐸 ∈ Cat ) )