Theorem vtxdginducedm1lem2

Description: Lemma 2 for vtxdginducedm1 : the domain of 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	vtxdginducedm1lem2	|- dom ( iEdg ` S ) = I

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	1 2 3 4 5 6	vtxdginducedm1lem1	|- ( iEdg ` S ) = P
8	7 5	eqtri	|- ( iEdg ` S ) = ( E |` I )
9	8	dmeqi	|- dom ( iEdg ` S ) = dom ( E |` I )
10	4	ssrab3	|- I C_ dom E
11		ssdmres	|- ( I C_ dom E <-> dom ( E |` I ) = I )
12	10 11	mpbi	|- dom ( E |` I ) = I
13	9 12	eqtri	|- dom ( iEdg ` S ) = I