This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. FinUSGraph /\ N e. V ) -> ( ( _I |` { p e. ( Edg ` <. V , E >. ) | N e/ p } ) e. Fin -> E e. Fin ) )

Proof

Step Hyp Ref Expression
1 residfi 
 |-  ( ( _I |` { p e. ( Edg ` <. V , E >. ) | N e/ p } ) e. Fin <-> { p e. ( Edg ` <. V , E >. ) | N e/ p } e. Fin )
2 fusgrusgr 
 |-  ( <. V , E >. e. FinUSGraph -> <. V , E >. e. USGraph )
3 eqid 
 |-  ( iEdg ` <. V , E >. ) = ( iEdg ` <. V , E >. )
4 eqid 
 |-  ( Edg ` <. V , E >. ) = ( Edg ` <. V , E >. )
5 3 4 usgredgffibi 
 |-  ( <. V , E >. e. USGraph -> ( ( Edg ` <. V , E >. ) e. Fin <-> ( iEdg ` <. V , E >. ) e. Fin ) )
6 2 5 syl 
 |-  ( <. V , E >. e. FinUSGraph -> ( ( Edg ` <. V , E >. ) e. Fin <-> ( iEdg ` <. V , E >. ) e. Fin ) )
7 6 3ad2ant2 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. FinUSGraph /\ N e. V ) -> ( ( Edg ` <. V , E >. ) e. Fin <-> ( iEdg ` <. V , E >. ) e. Fin ) )
8 simp2 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. FinUSGraph /\ N e. V ) -> <. V , E >. e. FinUSGraph )
9 opvtxfv 
 |-  ( ( V e. X /\ E e. Y ) -> ( Vtx ` <. V , E >. ) = V )
10 9 eqcomd 
 |-  ( ( V e. X /\ E e. Y ) -> V = ( Vtx ` <. V , E >. ) )
11 10 eleq2d 
 |-  ( ( V e. X /\ E e. Y ) -> ( N e. V <-> N e. ( Vtx ` <. V , E >. ) ) )
12 11 biimpa 
 |-  ( ( ( V e. X /\ E e. Y ) /\ N e. V ) -> N e. ( Vtx ` <. V , E >. ) )
13 eqid 
 |-  ( Vtx ` <. V , E >. ) = ( Vtx ` <. V , E >. )
14 eqid 
 |-  { p e. ( Edg ` <. V , E >. ) | N e/ p } = { p e. ( Edg ` <. V , E >. ) | N e/ p }
15 13 4 14 usgrfilem 
 |-  ( ( <. V , E >. e. FinUSGraph /\ N e. ( Vtx ` <. V , E >. ) ) -> ( ( Edg ` <. V , E >. ) e. Fin <-> { p e. ( Edg ` <. V , E >. ) | N e/ p } e. Fin ) )
16 8 12 15 3imp3i2an 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. FinUSGraph /\ N e. V ) -> ( ( Edg ` <. V , E >. ) e. Fin <-> { p e. ( Edg ` <. V , E >. ) | N e/ p } e. Fin ) )
17 opiedgfv 
 |-  ( ( V e. X /\ E e. Y ) -> ( iEdg ` <. V , E >. ) = E )
18 17 eleq1d 
 |-  ( ( V e. X /\ E e. Y ) -> ( ( iEdg ` <. V , E >. ) e. Fin <-> E e. Fin ) )
19 18 3ad2ant1 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. FinUSGraph /\ N e. V ) -> ( ( iEdg ` <. V , E >. ) e. Fin <-> E e. Fin ) )
20 7 16 19 3bitr3rd 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. FinUSGraph /\ N e. V ) -> ( E e. Fin <-> { p e. ( Edg ` <. V , E >. ) | N e/ p } e. Fin ) )
21 20 biimprd 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. FinUSGraph /\ N e. V ) -> ( { p e. ( Edg ` <. V , E >. ) | N e/ p } e. Fin -> E e. Fin ) )
22 1 21 biimtrid 
 |-  ( ( ( V e. X /\ E e. Y ) /\ <. V , E >. e. FinUSGraph /\ N e. V ) -> ( ( _I |` { p e. ( Edg ` <. V , E >. ) | N e/ p } ) e. Fin -> E e. Fin ) )