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