Theorem vtxdginducedm1lem3

Description: Lemma 3 for vtxdginducedm1 : an edge 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=\mathrm{Vtx}\left(G\right)$$
	vtxdginducedm1.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
	vtxdginducedm1.k	$$⊢K=V\setminus \left\{N\right\}$$
	vtxdginducedm1.i	$$⊢I=\left\{i\in \mathrm{dom}E|N\notin E\left(i\right)\right\}$$
	vtxdginducedm1.p	$$⊢P={E\upharpoonright }_I$$
	vtxdginducedm1.s	$$⊢S=⟨K,P⟩$$
Assertion	vtxdginducedm1lem3	$$⊢H\in I\to \mathrm{iEdg}\left(S\right)\left(H\right)=E\left(H\right)$$

Proof

Step	Hyp	Ref	Expression
1		vtxdginducedm1.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		vtxdginducedm1.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
3		vtxdginducedm1.k	$$⊢K=V\setminus \left\{N\right\}$$
4		vtxdginducedm1.i	$$⊢I=\left\{i\in \mathrm{dom}E|N\notin E\left(i\right)\right\}$$
5		vtxdginducedm1.p	$$⊢P={E\upharpoonright }_I$$
6		vtxdginducedm1.s	$$⊢S=⟨K,P⟩$$
7	1 2 3 4 5 6	vtxdginducedm1lem1	$$⊢\mathrm{iEdg}\left(S\right)=P$$
8	7 5	eqtri	$$⊢\mathrm{iEdg}\left(S\right)={E\upharpoonright }_I$$
9	8	fveq1i	$$⊢\mathrm{iEdg}\left(S\right)\left(H\right)=\left({E\upharpoonright }_I\right)\left(H\right)$$
10		fvres	$$⊢H\in I\to \left({E\upharpoonright }_I\right)\left(H\right)=E\left(H\right)$$
11	9 10	syl5eq	$$⊢H\in I\to \mathrm{iEdg}\left(S\right)\left(H\right)=E\left(H\right)$$