Metamath Proof Explorer


Theorem vtxdginducedm1lem4

Description: Lemma 4 for vtxdginducedm1 . (Contributed by AV, 17-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
vtxdginducedm1.j J = i dom E | N E i
Assertion vtxdginducedm1lem4 W V N k J | E k = W = 0

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 vtxdginducedm1.j J = i dom E | N E i
8 fveq2 i = k E i = E k
9 8 eleq2d i = k N E i N E k
10 9 7 elrab2 k J k dom E N E k
11 eldifsn W V N W V W N
12 df-ne W N ¬ W = N
13 eleq2 E k = W N E k N W
14 elsni N W N = W
15 14 eqcomd N W W = N
16 13 15 syl6bi E k = W N E k W = N
17 16 com12 N E k E k = W W = N
18 17 con3rr3 ¬ W = N N E k ¬ E k = W
19 12 18 sylbi W N N E k ¬ E k = W
20 11 19 simplbiim W V N N E k ¬ E k = W
21 20 com12 N E k W V N ¬ E k = W
22 10 21 simplbiim k J W V N ¬ E k = W
23 22 impcom W V N k J ¬ E k = W
24 23 ralrimiva W V N k J ¬ E k = W
25 rabeq0 k J | E k = W = k J ¬ E k = W
26 24 25 sylibr W V N k J | E k = W =
27 2 fvexi E V
28 27 dmex dom E V
29 7 28 rab2ex k J | E k = W V
30 hasheq0 k J | E k = W V k J | E k = W = 0 k J | E k = W =
31 29 30 ax-mp k J | E k = W = 0 k J | E k = W =
32 26 31 sylibr W V N k J | E k = W = 0