# Metamath Proof Explorer

## Theorem uhgrspan1lem2

Description: Lemma 2 for uhgrspan1 . (Contributed by AV, 19-Nov-2020)

Ref Expression
Hypotheses uhgrspan1.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
uhgrspan1.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
uhgrspan1.f ${⊢}{F}=\left\{{i}\in \mathrm{dom}{I}|{N}\notin {I}\left({i}\right)\right\}$
uhgrspan1.s ${⊢}{S}=⟨{V}\setminus \left\{{N}\right\},{{I}↾}_{{F}}⟩$
Assertion uhgrspan1lem2 ${⊢}\mathrm{Vtx}\left({S}\right)={V}\setminus \left\{{N}\right\}$

### Proof

Step Hyp Ref Expression
1 uhgrspan1.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 uhgrspan1.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
3 uhgrspan1.f ${⊢}{F}=\left\{{i}\in \mathrm{dom}{I}|{N}\notin {I}\left({i}\right)\right\}$
4 uhgrspan1.s ${⊢}{S}=⟨{V}\setminus \left\{{N}\right\},{{I}↾}_{{F}}⟩$
5 4 fveq2i ${⊢}\mathrm{Vtx}\left({S}\right)=\mathrm{Vtx}\left(⟨{V}\setminus \left\{{N}\right\},{{I}↾}_{{F}}⟩\right)$
6 1 2 3 uhgrspan1lem1 ${⊢}\left({V}\setminus \left\{{N}\right\}\in \mathrm{V}\wedge {{I}↾}_{{F}}\in \mathrm{V}\right)$
7 opvtxfv ${⊢}\left({V}\setminus \left\{{N}\right\}\in \mathrm{V}\wedge {{I}↾}_{{F}}\in \mathrm{V}\right)\to \mathrm{Vtx}\left(⟨{V}\setminus \left\{{N}\right\},{{I}↾}_{{F}}⟩\right)={V}\setminus \left\{{N}\right\}$
8 6 7 ax-mp ${⊢}\mathrm{Vtx}\left(⟨{V}\setminus \left\{{N}\right\},{{I}↾}_{{F}}⟩\right)={V}\setminus \left\{{N}\right\}$
9 5 8 eqtri ${⊢}\mathrm{Vtx}\left({S}\right)={V}\setminus \left\{{N}\right\}$