# Metamath Proof Explorer

## Theorem upgrres1lem1

Description: Lemma 1 for upgrres1 . (Contributed by AV, 7-Nov-2020)

Ref Expression
Hypotheses upgrres1.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
upgrres1.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
upgrres1.f ${⊢}{F}=\left\{{e}\in {E}|{N}\notin {e}\right\}$
Assertion upgrres1lem1 ${⊢}\left({V}\setminus \left\{{N}\right\}\in \mathrm{V}\wedge {\mathrm{I}↾}_{{F}}\in \mathrm{V}\right)$

### Proof

Step Hyp Ref Expression
1 upgrres1.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 upgrres1.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 upgrres1.f ${⊢}{F}=\left\{{e}\in {E}|{N}\notin {e}\right\}$
4 1 fvexi ${⊢}{V}\in \mathrm{V}$
5 4 difexi ${⊢}{V}\setminus \left\{{N}\right\}\in \mathrm{V}$
6 2 fvexi ${⊢}{E}\in \mathrm{V}$
7 3 6 rabex2 ${⊢}{F}\in \mathrm{V}$
8 resiexg ${⊢}{F}\in \mathrm{V}\to {\mathrm{I}↾}_{{F}}\in \mathrm{V}$
9 7 8 ax-mp ${⊢}{\mathrm{I}↾}_{{F}}\in \mathrm{V}$
10 5 9 pm3.2i ${⊢}\left({V}\setminus \left\{{N}\right\}\in \mathrm{V}\wedge {\mathrm{I}↾}_{{F}}\in \mathrm{V}\right)$