# Metamath Proof Explorer

## Theorem uhgrspan1lem3

Description: Lemma 3 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 uhgrspan1lem3 ${⊢}\mathrm{iEdg}\left({S}\right)={{I}↾}_{{F}}$

### 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{iEdg}\left({S}\right)=\mathrm{iEdg}\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 opiedgfv ${⊢}\left({V}\setminus \left\{{N}\right\}\in \mathrm{V}\wedge {{I}↾}_{{F}}\in \mathrm{V}\right)\to \mathrm{iEdg}\left(⟨{V}\setminus \left\{{N}\right\},{{I}↾}_{{F}}⟩\right)={{I}↾}_{{F}}$
8 6 7 ax-mp ${⊢}\mathrm{iEdg}\left(⟨{V}\setminus \left\{{N}\right\},{{I}↾}_{{F}}⟩\right)={{I}↾}_{{F}}$
9 5 8 eqtri ${⊢}\mathrm{iEdg}\left({S}\right)={{I}↾}_{{F}}$