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

Metamath Proof Explorer

Theorem ressco

Description: comp is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017)

Ref Expression
Hypotheses resshom.1 ⊢ D = C ↾ 𝑠 A
ressco.2 ⊢ · ˙ = comp ⁡ C
Assertion ressco ⊢ A ∈ V → · ˙ = comp ⁡ D

Proof

Step Hyp Ref Expression
1 resshom.1 ⊢ D = C ↾ 𝑠 A
2 ressco.2 ⊢ · ˙ = comp ⁡ C
3 ccoid ⊢ comp = Slot comp ⁡ ndx
4 slotsbhcdif ⊢ Base ndx ≠ Hom ⁡ ndx ∧ Base ndx ≠ comp ⁡ ndx ∧ Hom ⁡ ndx ≠ comp ⁡ ndx
5 simp2 ⊢ Base ndx ≠ Hom ⁡ ndx ∧ Base ndx ≠ comp ⁡ ndx ∧ Hom ⁡ ndx ≠ comp ⁡ ndx → Base ndx ≠ comp ⁡ ndx
6 5 necomd ⊢ Base ndx ≠ Hom ⁡ ndx ∧ Base ndx ≠ comp ⁡ ndx ∧ Hom ⁡ ndx ≠ comp ⁡ ndx → comp ⁡ ndx ≠ Base ndx
7 4 6 ax-mp ⊢ comp ⁡ ndx ≠ Base ndx
8 1 2 3 7 resseqnbas ⊢ A ∈ V → · ˙ = comp ⁡ D