# Metamath Proof Explorer

## Theorem fusgrfisstep

Description: Induction step in fusgrfis : In a finite simple graph, the number of edges is finite if the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 5-Jan-2018) (Revised by AV, 23-Oct-2020)

Ref Expression
Assertion fusgrfisstep ${⊢}\left(\left({V}\in {X}\wedge {E}\in {Y}\right)\wedge ⟨{V},{E}⟩\in \mathrm{FinUSGraph}\wedge {N}\in {V}\right)\to \left({\mathrm{I}↾}_{\left\{{p}\in \mathrm{Edg}\left(⟨{V},{E}⟩\right)|{N}\notin {p}\right\}}\in \mathrm{Fin}\to {E}\in \mathrm{Fin}\right)$

### Proof

Step Hyp Ref Expression
1 residfi ${⊢}{\mathrm{I}↾}_{\left\{{p}\in \mathrm{Edg}\left(⟨{V},{E}⟩\right)|{N}\notin {p}\right\}}\in \mathrm{Fin}↔\left\{{p}\in \mathrm{Edg}\left(⟨{V},{E}⟩\right)|{N}\notin {p}\right\}\in \mathrm{Fin}$
2 fusgrusgr ${⊢}⟨{V},{E}⟩\in \mathrm{FinUSGraph}\to ⟨{V},{E}⟩\in \mathrm{USGraph}$
3 eqid ${⊢}\mathrm{iEdg}\left(⟨{V},{E}⟩\right)=\mathrm{iEdg}\left(⟨{V},{E}⟩\right)$
4 eqid ${⊢}\mathrm{Edg}\left(⟨{V},{E}⟩\right)=\mathrm{Edg}\left(⟨{V},{E}⟩\right)$
5 3 4 usgredgffibi ${⊢}⟨{V},{E}⟩\in \mathrm{USGraph}\to \left(\mathrm{Edg}\left(⟨{V},{E}⟩\right)\in \mathrm{Fin}↔\mathrm{iEdg}\left(⟨{V},{E}⟩\right)\in \mathrm{Fin}\right)$
6 2 5 syl ${⊢}⟨{V},{E}⟩\in \mathrm{FinUSGraph}\to \left(\mathrm{Edg}\left(⟨{V},{E}⟩\right)\in \mathrm{Fin}↔\mathrm{iEdg}\left(⟨{V},{E}⟩\right)\in \mathrm{Fin}\right)$
7 6 3ad2ant2 ${⊢}\left(\left({V}\in {X}\wedge {E}\in {Y}\right)\wedge ⟨{V},{E}⟩\in \mathrm{FinUSGraph}\wedge {N}\in {V}\right)\to \left(\mathrm{Edg}\left(⟨{V},{E}⟩\right)\in \mathrm{Fin}↔\mathrm{iEdg}\left(⟨{V},{E}⟩\right)\in \mathrm{Fin}\right)$
8 simp2 ${⊢}\left(\left({V}\in {X}\wedge {E}\in {Y}\right)\wedge ⟨{V},{E}⟩\in \mathrm{FinUSGraph}\wedge {N}\in {V}\right)\to ⟨{V},{E}⟩\in \mathrm{FinUSGraph}$
9 opvtxfv ${⊢}\left({V}\in {X}\wedge {E}\in {Y}\right)\to \mathrm{Vtx}\left(⟨{V},{E}⟩\right)={V}$
10 9 eqcomd ${⊢}\left({V}\in {X}\wedge {E}\in {Y}\right)\to {V}=\mathrm{Vtx}\left(⟨{V},{E}⟩\right)$
11 10 eleq2d ${⊢}\left({V}\in {X}\wedge {E}\in {Y}\right)\to \left({N}\in {V}↔{N}\in \mathrm{Vtx}\left(⟨{V},{E}⟩\right)\right)$
12 11 biimpa ${⊢}\left(\left({V}\in {X}\wedge {E}\in {Y}\right)\wedge {N}\in {V}\right)\to {N}\in \mathrm{Vtx}\left(⟨{V},{E}⟩\right)$
13 eqid ${⊢}\mathrm{Vtx}\left(⟨{V},{E}⟩\right)=\mathrm{Vtx}\left(⟨{V},{E}⟩\right)$
14 eqid ${⊢}\left\{{p}\in \mathrm{Edg}\left(⟨{V},{E}⟩\right)|{N}\notin {p}\right\}=\left\{{p}\in \mathrm{Edg}\left(⟨{V},{E}⟩\right)|{N}\notin {p}\right\}$
15 13 4 14 usgrfilem ${⊢}\left(⟨{V},{E}⟩\in \mathrm{FinUSGraph}\wedge {N}\in \mathrm{Vtx}\left(⟨{V},{E}⟩\right)\right)\to \left(\mathrm{Edg}\left(⟨{V},{E}⟩\right)\in \mathrm{Fin}↔\left\{{p}\in \mathrm{Edg}\left(⟨{V},{E}⟩\right)|{N}\notin {p}\right\}\in \mathrm{Fin}\right)$
16 8 12 15 3imp3i2an ${⊢}\left(\left({V}\in {X}\wedge {E}\in {Y}\right)\wedge ⟨{V},{E}⟩\in \mathrm{FinUSGraph}\wedge {N}\in {V}\right)\to \left(\mathrm{Edg}\left(⟨{V},{E}⟩\right)\in \mathrm{Fin}↔\left\{{p}\in \mathrm{Edg}\left(⟨{V},{E}⟩\right)|{N}\notin {p}\right\}\in \mathrm{Fin}\right)$
17 opiedgfv ${⊢}\left({V}\in {X}\wedge {E}\in {Y}\right)\to \mathrm{iEdg}\left(⟨{V},{E}⟩\right)={E}$
18 17 eleq1d ${⊢}\left({V}\in {X}\wedge {E}\in {Y}\right)\to \left(\mathrm{iEdg}\left(⟨{V},{E}⟩\right)\in \mathrm{Fin}↔{E}\in \mathrm{Fin}\right)$
19 18 3ad2ant1 ${⊢}\left(\left({V}\in {X}\wedge {E}\in {Y}\right)\wedge ⟨{V},{E}⟩\in \mathrm{FinUSGraph}\wedge {N}\in {V}\right)\to \left(\mathrm{iEdg}\left(⟨{V},{E}⟩\right)\in \mathrm{Fin}↔{E}\in \mathrm{Fin}\right)$
20 7 16 19 3bitr3rd ${⊢}\left(\left({V}\in {X}\wedge {E}\in {Y}\right)\wedge ⟨{V},{E}⟩\in \mathrm{FinUSGraph}\wedge {N}\in {V}\right)\to \left({E}\in \mathrm{Fin}↔\left\{{p}\in \mathrm{Edg}\left(⟨{V},{E}⟩\right)|{N}\notin {p}\right\}\in \mathrm{Fin}\right)$
21 20 biimprd ${⊢}\left(\left({V}\in {X}\wedge {E}\in {Y}\right)\wedge ⟨{V},{E}⟩\in \mathrm{FinUSGraph}\wedge {N}\in {V}\right)\to \left(\left\{{p}\in \mathrm{Edg}\left(⟨{V},{E}⟩\right)|{N}\notin {p}\right\}\in \mathrm{Fin}\to {E}\in \mathrm{Fin}\right)$
22 1 21 syl5bi ${⊢}\left(\left({V}\in {X}\wedge {E}\in {Y}\right)\wedge ⟨{V},{E}⟩\in \mathrm{FinUSGraph}\wedge {N}\in {V}\right)\to \left({\mathrm{I}↾}_{\left\{{p}\in \mathrm{Edg}\left(⟨{V},{E}⟩\right)|{N}\notin {p}\right\}}\in \mathrm{Fin}\to {E}\in \mathrm{Fin}\right)$