Theorem vtxdginducedm1lem1

Description: Lemma 1 for vtxdginducedm1 : the edge function in the induced subgraph S of a pseudograph G obtained by removing one vertex N . (Contributed by AV, 16-Dec-2021)

	Ref	Expression
Hypotheses	vtxdginducedm1.v	|- V = ( Vtx ` G )
	vtxdginducedm1.e	|- E = ( iEdg ` G )
	vtxdginducedm1.k	|- K = ( V \ { N } )
	vtxdginducedm1.i	|- I = { i e. dom E | N e/ ( E ` i ) }
	vtxdginducedm1.p	|- P = ( E |` I )
	vtxdginducedm1.s	|- S = <. K , P >.
Assertion	vtxdginducedm1lem1	|- ( iEdg ` S ) = P

Proof

Step	Hyp	Ref	Expression
1		vtxdginducedm1.v	|- V = ( Vtx ` G )
2		vtxdginducedm1.e	|- E = ( iEdg ` G )
3		vtxdginducedm1.k	|- K = ( V \ { N } )
4		vtxdginducedm1.i	|- I = { i e. dom E | N e/ ( E ` i ) }
5		vtxdginducedm1.p	|- P = ( E |` I )
6		vtxdginducedm1.s	|- S = <. K , P >.
7	6	fveq2i	|- ( iEdg ` S ) = ( iEdg ` <. K , P >. )
8	1	fvexi	|- V e. _V
9	8	difexi	|- ( V \ { N } ) e. _V
10	3 9	eqeltri	|- K e. _V
11	2	fvexi	|- E e. _V
12	11	resex	|- ( E |` I ) e. _V
13	5 12	eqeltri	|- P e. _V
14	10 13	opiedgfvi	|- ( iEdg ` <. K , P >. ) = P
15	7 14	eqtri	|- ( iEdg ` S ) = P