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	syl5bi	|- ( ( ( 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 ) )