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

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	dmeqi	$$⊢\mathrm{dom}\mathrm{iEdg}\left(S\right)=\mathrm{dom}\left({E\upharpoonright }_I\right)$$
10	4	ssrab3	$$⊢I\subseteq \mathrm{dom}E$$
11		ssdmres	$$⊢I\subseteq \mathrm{dom}E\leftrightarrow \mathrm{dom}\left({E\upharpoonright }_I\right)=I$$
12	10 11	mpbi	$$⊢\mathrm{dom}\left({E\upharpoonright }_I\right)=I$$
13	9 12	eqtri	$$⊢\mathrm{dom}\mathrm{iEdg}\left(S\right)=I$$