# Metamath Proof Explorer

## Theorem rescbas

Description: Base set of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses rescbas.d ${⊢}{D}={C}{↾}_{\mathrm{cat}}{H}$
rescbas.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
rescbas.c ${⊢}{\phi }\to {C}\in {V}$
rescbas.h ${⊢}{\phi }\to {H}Fn\left({S}×{S}\right)$
rescbas.s ${⊢}{\phi }\to {S}\subseteq {B}$
Assertion rescbas ${⊢}{\phi }\to {S}={\mathrm{Base}}_{{D}}$

### Proof

Step Hyp Ref Expression
1 rescbas.d ${⊢}{D}={C}{↾}_{\mathrm{cat}}{H}$
2 rescbas.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
3 rescbas.c ${⊢}{\phi }\to {C}\in {V}$
4 rescbas.h ${⊢}{\phi }\to {H}Fn\left({S}×{S}\right)$
5 rescbas.s ${⊢}{\phi }\to {S}\subseteq {B}$
6 baseid ${⊢}\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$
7 1re ${⊢}1\in ℝ$
8 1nn ${⊢}1\in ℕ$
9 4nn0 ${⊢}4\in {ℕ}_{0}$
10 1nn0 ${⊢}1\in {ℕ}_{0}$
11 1lt10 ${⊢}1<10$
12 8 9 10 11 declti ${⊢}1<14$
13 7 12 ltneii ${⊢}1\ne 14$
14 basendx ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}=1$
15 homndx ${⊢}\mathrm{Hom}\left(\mathrm{ndx}\right)=14$
16 14 15 neeq12i ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)↔1\ne 14$
17 13 16 mpbir ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$
18 6 17 setsnid ${⊢}{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}={\mathrm{Base}}_{\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right)}$
19 eqid ${⊢}{C}{↾}_{𝑠}{S}={C}{↾}_{𝑠}{S}$
20 19 2 ressbas2 ${⊢}{S}\subseteq {B}\to {S}={\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}$
21 5 20 syl ${⊢}{\phi }\to {S}={\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}$
22 2 fvexi ${⊢}{B}\in \mathrm{V}$
23 22 ssex ${⊢}{S}\subseteq {B}\to {S}\in \mathrm{V}$
24 5 23 syl ${⊢}{\phi }\to {S}\in \mathrm{V}$
25 1 3 24 4 rescval2 ${⊢}{\phi }\to {D}=\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩$
26 25 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{D}}={\mathrm{Base}}_{\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right)}$
27 18 21 26 3eqtr4a ${⊢}{\phi }\to {S}={\mathrm{Base}}_{{D}}$