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 ⊢ 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 vtxdginducedm1lem1 ⊢ iEdg ⁡ S = P

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 6 fveq2i ⊢ iEdg ⁡ S = iEdg ⁡ K P
8 1 fvexi ⊢ V ∈ V
9 8 difexi ⊢ V ∖ N ∈ V
10 3 9 eqeltri ⊢ K ∈ V
11 2 fvexi ⊢ E ∈ V
12 11 resex ⊢ E ↾ I ∈ V
13 5 12 eqeltri ⊢ P ∈ V
14 10 13 opiedgfvi ⊢ iEdg ⁡ K P = P
15 7 14 eqtri ⊢ iEdg ⁡ S = P