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=\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	vtxdginducedm1lem1	$$⊢\mathrm{iEdg}\left(S\right)=P$$

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	6	fveq2i	$$⊢\mathrm{iEdg}\left(S\right)=\mathrm{iEdg}\left(⟨K,P⟩\right)$$
8	1	fvexi	$$⊢V\in \mathrm{V}$$
9	8	difexi	$$⊢V\setminus \left\{N\right\}\in \mathrm{V}$$
10	3 9	eqeltri	$$⊢K\in \mathrm{V}$$
11	2	fvexi	$$⊢E\in \mathrm{V}$$
12	11	resex	$$⊢{E\upharpoonright }_I\in \mathrm{V}$$
13	5 12	eqeltri	$$⊢P\in \mathrm{V}$$
14	10 13	opiedgfvi	$$⊢\mathrm{iEdg}\left(⟨K,P⟩\right)=P$$
15	7 14	eqtri	$$⊢\mathrm{iEdg}\left(S\right)=P$$