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

Metamath Proof Explorer

Theorem rescco

Description: Composition in the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by AV, 13-Oct-2024)

Ref Expression
Hypotheses rescbas.d ⊢ 𝐷 = ( 𝐶 ↾cat 𝐻 )
rescbas.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
rescbas.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
rescbas.h ⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
rescbas.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
rescco.o ⊢ · = ( comp ‘ 𝐶 )
Assertion rescco ( 𝜑 → · = ( comp ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 rescbas.d ⊢ 𝐷 = ( 𝐶 ↾cat 𝐻 )
2 rescbas.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 rescbas.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4 rescbas.h ⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
5 rescbas.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
6 rescco.o ⊢ · = ( comp ‘ 𝐶 )
7 ccoid ⊢ comp = Slot ( comp ‘ ndx )
8 slotsbhcdif ⊢ ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) )
9 simp3 ⊢ ( ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) ) → ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) )
10 9 necomd ⊢ ( ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) ) → ( comp ‘ ndx ) ≠ ( Hom ‘ ndx ) )
11 8 10 ax-mp ⊢ ( comp ‘ ndx ) ≠ ( Hom ‘ ndx )
12 7 11 setsnid ⊢ ( comp ‘ ( 𝐶 ↾s 𝑆 ) ) = ( comp ‘ ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
13 2 fvexi ⊢ 𝐵 ∈ V
14 13 ssex ⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 ∈ V )
15 5 14 syl ⊢ ( 𝜑 → 𝑆 ∈ V )
16 eqid ⊢ ( 𝐶 ↾s 𝑆 ) = ( 𝐶 ↾s 𝑆 )
17 16 6 ressco ⊢ ( 𝑆 ∈ V → · = ( comp ‘ ( 𝐶 ↾s 𝑆 ) ) )
18 15 17 syl ⊢ ( 𝜑 → · = ( comp ‘ ( 𝐶 ↾s 𝑆 ) ) )
19 1 3 15 4 rescval2 ⊢ ( 𝜑 → 𝐷 = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
20 19 fveq2d ⊢ ( 𝜑 → ( comp ‘ 𝐷 ) = ( comp ‘ ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ) )
21 12 18 20 3eqtr4a ⊢ ( 𝜑 → · = ( comp ‘ 𝐷 ) )