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

Metamath Proof Explorer

Theorem rescbas

Description: Base set of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by AV, 18-Oct-2024)

Ref Expression
Hypotheses rescbas.d ⊢ D = C ↾ cat H
rescbas.b ⊢ B = Base C
rescbas.c ⊢ φ → C ∈ V
rescbas.h ⊢ φ → H Fn S × S
rescbas.s ⊢ φ → S ⊆ B
Assertion rescbas ⊢ φ → S = Base D

Proof

Step Hyp Ref Expression
1 rescbas.d ⊢ D = C ↾ cat H
2 rescbas.b ⊢ B = Base C
3 rescbas.c ⊢ φ → C ∈ V
4 rescbas.h ⊢ φ → H Fn S × S
5 rescbas.s ⊢ φ → S ⊆ B
6 baseid ⊢ Base = Slot Base ndx
7 slotsbhcdif ⊢ Base ndx ≠ Hom ⁡ ndx ∧ Base ndx ≠ comp ⁡ ndx ∧ Hom ⁡ ndx ≠ comp ⁡ ndx
8 7 simp1i ⊢ Base ndx ≠ Hom ⁡ ndx
9 6 8 setsnid ⊢ Base C ↾ 𝑠 S = Base C ↾ 𝑠 S sSet Hom ⁡ ndx H
10 eqid ⊢ C ↾ 𝑠 S = C ↾ 𝑠 S
11 10 2 ressbas2 ⊢ S ⊆ B → S = Base C ↾ 𝑠 S
12 5 11 syl ⊢ φ → S = Base C ↾ 𝑠 S
13 2 fvexi ⊢ B ∈ V
14 13 ssex ⊢ S ⊆ B → S ∈ V
15 5 14 syl ⊢ φ → S ∈ V
16 1 3 15 4 rescval2 ⊢ φ → D = C ↾ 𝑠 S sSet Hom ⁡ ndx H
17 16 fveq2d ⊢ φ → Base D = Base C ↾ 𝑠 S sSet Hom ⁡ ndx H
18 9 12 17 3eqtr4a ⊢ φ → S = Base D