# Metamath Proof Explorer

## Theorem setsvtx

Description: The vertices of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 18-Jan-2020) (Revised by AV, 16-Nov-2021)

Ref Expression
Hypotheses setsvtx.i ${⊢}{I}=\mathrm{ef}\left(\mathrm{ndx}\right)$
setsvtx.s ${⊢}{\phi }\to {G}\mathrm{Struct}{X}$
setsvtx.b ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}{G}$
setsvtx.e ${⊢}{\phi }\to {E}\in {W}$
Assertion setsvtx ${⊢}{\phi }\to \mathrm{Vtx}\left({G}\mathrm{sSet}⟨{I},{E}⟩\right)={\mathrm{Base}}_{{G}}$

### Proof

Step Hyp Ref Expression
1 setsvtx.i ${⊢}{I}=\mathrm{ef}\left(\mathrm{ndx}\right)$
2 setsvtx.s ${⊢}{\phi }\to {G}\mathrm{Struct}{X}$
3 setsvtx.b ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}{G}$
4 setsvtx.e ${⊢}{\phi }\to {E}\in {W}$
5 1 fvexi ${⊢}{I}\in \mathrm{V}$
6 5 a1i ${⊢}{\phi }\to {I}\in \mathrm{V}$
7 2 6 4 setsn0fun ${⊢}{\phi }\to \mathrm{Fun}\left(\left({G}\mathrm{sSet}⟨{I},{E}⟩\right)\setminus \left\{\varnothing \right\}\right)$
8 1 eqcomi ${⊢}\mathrm{ef}\left(\mathrm{ndx}\right)={I}$
9 8 preq2i ${⊢}\left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ef}\left(\mathrm{ndx}\right)\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},{I}\right\}$
10 2 6 4 3 basprssdmsets ${⊢}{\phi }\to \left\{{\mathrm{Base}}_{\mathrm{ndx}},{I}\right\}\subseteq \mathrm{dom}\left({G}\mathrm{sSet}⟨{I},{E}⟩\right)$
11 9 10 eqsstrid ${⊢}{\phi }\to \left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ef}\left(\mathrm{ndx}\right)\right\}\subseteq \mathrm{dom}\left({G}\mathrm{sSet}⟨{I},{E}⟩\right)$
12 funvtxval ${⊢}\left(\mathrm{Fun}\left(\left({G}\mathrm{sSet}⟨{I},{E}⟩\right)\setminus \left\{\varnothing \right\}\right)\wedge \left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ef}\left(\mathrm{ndx}\right)\right\}\subseteq \mathrm{dom}\left({G}\mathrm{sSet}⟨{I},{E}⟩\right)\right)\to \mathrm{Vtx}\left({G}\mathrm{sSet}⟨{I},{E}⟩\right)={\mathrm{Base}}_{\left({G}\mathrm{sSet}⟨{I},{E}⟩\right)}$
13 7 11 12 syl2anc ${⊢}{\phi }\to \mathrm{Vtx}\left({G}\mathrm{sSet}⟨{I},{E}⟩\right)={\mathrm{Base}}_{\left({G}\mathrm{sSet}⟨{I},{E}⟩\right)}$
14 baseid ${⊢}\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$
15 slotsbaseefdif ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{ef}\left(\mathrm{ndx}\right)$
16 15 1 neeqtrri ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\ne {I}$
17 14 16 setsnid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{\left({G}\mathrm{sSet}⟨{I},{E}⟩\right)}$
18 13 17 syl6eqr ${⊢}{\phi }\to \mathrm{Vtx}\left({G}\mathrm{sSet}⟨{I},{E}⟩\right)={\mathrm{Base}}_{{G}}$