Theorem resccatlem

Description: Lemma for resccat . (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	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
	resccatlem.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
Assertion	resccatlem	⊢ ( 𝜑 → ( 𝐷 ∈ 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		resccatlem.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
11	4 3	homffn	⊢ 𝐽 Fn ( 𝑆 × 𝑆 )
12	11	a1i	⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
13	1 2 10 12 9	reschomf	⊢ ( 𝜑 → 𝐽 = ( Homf ‘ 𝐷 ) )
14	13 4	eqtr3di	⊢ ( 𝜑 → ( Homf ‘ 𝐷 ) = ( Homf ‘ 𝐸 ) )
15	7	ralrimivva	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) )
16	15	ralrimivvva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) )
17		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
18		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
19	1 2 10 12 9	rescbas	⊢ ( 𝜑 → 𝑆 = ( Base ‘ 𝐷 ) )
20	3	a1i	⊢ ( 𝜑 → 𝑆 = ( Base ‘ 𝐸 ) )
21	17 6 18 19 20 14	comfeq	⊢ ( 𝜑 → ( ( compf ‘ 𝐷 ) = ( compf ‘ 𝐸 ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ) )
22	1 2 10 12 9	reschom	⊢ ( 𝜑 → 𝐽 = ( Hom ‘ 𝐷 ) )
23	22	oveqd	⊢ ( 𝜑 → ( 𝑥 𝐽 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) )
24	22	oveqd	⊢ ( 𝜑 → ( 𝑦 𝐽 𝑧 ) = ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) )
25	1 2 10 12 9 5	rescco	⊢ ( 𝜑 → · = ( comp ‘ 𝐷 ) )
26	25	oveqd	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) )
27	26	oveqd	⊢ ( 𝜑 → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) )
28	27	eqeq1d	⊢ ( 𝜑 → ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ↔ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ) )
29	24 28	raleqbidv	⊢ ( 𝜑 → ( ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ↔ ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ) )
30	23 29	raleqbidv	⊢ ( 𝜑 → ( ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ↔ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ) )
31	30	3ralbidv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ) )
32	21 31	bitr4d	⊢ ( 𝜑 → ( ( compf ‘ 𝐷 ) = ( compf ‘ 𝐸 ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∙ 𝑧 ) 𝑓 ) ) )
33	16 32	mpbird	⊢ ( 𝜑 → ( compf ‘ 𝐷 ) = ( compf ‘ 𝐸 ) )
34	1	ovexi	⊢ 𝐷 ∈ V
35	34	a1i	⊢ ( 𝜑 → 𝐷 ∈ V )
36	14 33 35 8	catpropd	⊢ ( 𝜑 → ( 𝐷 ∈ Cat ↔ 𝐸 ∈ Cat ) )