# Metamath Proof Explorer

## Theorem funvtxval

Description: The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 22-Sep-2020) (Revised by AV, 7-Jun-2021) (Revised by AV, 12-Nov-2021)

Ref Expression
Assertion funvtxval ${⊢}\left(\mathrm{Fun}\left({G}\setminus \left\{\varnothing \right\}\right)\wedge \left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ef}\left(\mathrm{ndx}\right)\right\}\subseteq \mathrm{dom}{G}\right)\to \mathrm{Vtx}\left({G}\right)={\mathrm{Base}}_{{G}}$

### Proof

Step Hyp Ref Expression
1 slotsbaseefdif ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{ef}\left(\mathrm{ndx}\right)$
2 fvex ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$
3 fvex ${⊢}\mathrm{ef}\left(\mathrm{ndx}\right)\in \mathrm{V}$
4 2 3 funvtxdm2val ${⊢}\left(\mathrm{Fun}\left({G}\setminus \left\{\varnothing \right\}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{ef}\left(\mathrm{ndx}\right)\wedge \left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ef}\left(\mathrm{ndx}\right)\right\}\subseteq \mathrm{dom}{G}\right)\to \mathrm{Vtx}\left({G}\right)={\mathrm{Base}}_{{G}}$
5 1 4 mp3an2 ${⊢}\left(\mathrm{Fun}\left({G}\setminus \left\{\varnothing \right\}\right)\wedge \left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ef}\left(\mathrm{ndx}\right)\right\}\subseteq \mathrm{dom}{G}\right)\to \mathrm{Vtx}\left({G}\right)={\mathrm{Base}}_{{G}}$