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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	vtxdginducedm1.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
	vtxdginducedm1.k	⊢ 𝐾 = ( 𝑉 ∖ { 𝑁 } )
	vtxdginducedm1.i	⊢ 𝐼 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
	vtxdginducedm1.p	⊢ 𝑃 = ( 𝐸 ↾ 𝐼 )
	vtxdginducedm1.s	⊢ 𝑆 = ⟨ 𝐾 , 𝑃 ⟩
Assertion	vtxdginducedm1lem2	⊢ dom ( iEdg ‘ 𝑆 ) = 𝐼

Proof

Step	Hyp	Ref	Expression
1		vtxdginducedm1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		vtxdginducedm1.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3		vtxdginducedm1.k	⊢ 𝐾 = ( 𝑉 ∖ { 𝑁 } )
4		vtxdginducedm1.i	⊢ 𝐼 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
5		vtxdginducedm1.p	⊢ 𝑃 = ( 𝐸 ↾ 𝐼 )
6		vtxdginducedm1.s	⊢ 𝑆 = ⟨ 𝐾 , 𝑃 ⟩
7	1 2 3 4 5 6	vtxdginducedm1lem1	⊢ ( iEdg ‘ 𝑆 ) = 𝑃
8	7 5	eqtri	⊢ ( iEdg ‘ 𝑆 ) = ( 𝐸 ↾ 𝐼 )
9	8	dmeqi	⊢ dom ( iEdg ‘ 𝑆 ) = dom ( 𝐸 ↾ 𝐼 )
10	4	ssrab3	⊢ 𝐼 ⊆ dom 𝐸
11		ssdmres	⊢ ( 𝐼 ⊆ dom 𝐸 ↔ dom ( 𝐸 ↾ 𝐼 ) = 𝐼 )
12	10 11	mpbi	⊢ dom ( 𝐸 ↾ 𝐼 ) = 𝐼
13	9 12	eqtri	⊢ dom ( iEdg ‘ 𝑆 ) = 𝐼