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 ⊢ V = Vtx ⁡ G
vtxdginducedm1.e ⊢ E = iEdg ⁡ G
vtxdginducedm1.k ⊢ K = V ∖ N
vtxdginducedm1.i ⊢ I = i ∈ dom ⁡ E | N ∉ E ⁡ i
vtxdginducedm1.p ⊢ P = E ↾ I
vtxdginducedm1.s ⊢ S = K P
Assertion vtxdginducedm1lem3 ⊢ H ∈ I → iEdg ⁡ S ⁡ H = E ⁡ H

Proof

Step Hyp Ref Expression
1 vtxdginducedm1.v ⊢ V = Vtx ⁡ G
2 vtxdginducedm1.e ⊢ E = iEdg ⁡ G
3 vtxdginducedm1.k ⊢ K = V ∖ N
4 vtxdginducedm1.i ⊢ I = i ∈ dom ⁡ E | N ∉ E ⁡ i
5 vtxdginducedm1.p ⊢ P = E ↾ I
6 vtxdginducedm1.s ⊢ S = K P
7 1 2 3 4 5 6 vtxdginducedm1lem1 ⊢ iEdg ⁡ S = P
8 7 5 eqtri ⊢ iEdg ⁡ S = E ↾ I
9 8 fveq1i ⊢ iEdg ⁡ S ⁡ H = E ↾ I ⁡ H
10 fvres ⊢ H ∈ I → E ↾ I ⁡ H = E ⁡ H
11 9 10 eqtrid ⊢ H ∈ I → iEdg ⁡ S ⁡ H = E ⁡ H