This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
		vtxdginducedm1.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
		vtxdginducedm1.k	⊢ 𝐾 = ( 𝑉 ∖ { 𝑁 } )
		vtxdginducedm1.i	⊢ 𝐼 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
		vtxdginducedm1.p	⊢ 𝑃 = ( 𝐸 ↾ 𝐼 )
		vtxdginducedm1.s	⊢ 𝑆 = ⟨ 𝐾 , 𝑃 ⟩
	Assertion	vtxdginducedm1lem1	⊢ ( 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	6	fveq2i	⊢ ( iEdg ‘ 𝑆 ) = ( iEdg ‘ ⟨ 𝐾 , 𝑃 ⟩ )
8	1	fvexi	⊢ 𝑉 ∈ V
9	8	difexi	⊢ ( 𝑉 ∖ { 𝑁 } ) ∈ V
10	3 9	eqeltri	⊢ 𝐾 ∈ V
11	2	fvexi	⊢ 𝐸 ∈ V
12	11	resex	⊢ ( 𝐸 ↾ 𝐼 ) ∈ V
13	5 12	eqeltri	⊢ 𝑃 ∈ V
14	10 13	opiedgfvi	⊢ ( iEdg ‘ ⟨ 𝐾 , 𝑃 ⟩ ) = 𝑃
15	7 14	eqtri	⊢ ( iEdg ‘ 𝑆 ) = 𝑃