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

Metamath Proof Explorer

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