Metamath Proof Explorer


Theorem vtxdginducedm1lem4

Description: Lemma 4 for vtxdginducedm1 . (Contributed by AV, 17-Dec-2021)

Ref Expression
Hypotheses vtxdginducedm1.v V=VtxG
vtxdginducedm1.e E=iEdgG
vtxdginducedm1.k K=VN
vtxdginducedm1.i I=idomE|NEi
vtxdginducedm1.p P=EI
vtxdginducedm1.s S=KP
vtxdginducedm1.j J=idomE|NEi
Assertion vtxdginducedm1lem4 WVNkJ|Ek=W=0

Proof

Step Hyp Ref Expression
1 vtxdginducedm1.v V=VtxG
2 vtxdginducedm1.e E=iEdgG
3 vtxdginducedm1.k K=VN
4 vtxdginducedm1.i I=idomE|NEi
5 vtxdginducedm1.p P=EI
6 vtxdginducedm1.s S=KP
7 vtxdginducedm1.j J=idomE|NEi
8 fveq2 i=kEi=Ek
9 8 eleq2d i=kNEiNEk
10 9 7 elrab2 kJkdomENEk
11 eldifsn WVNWVWN
12 df-ne WN¬W=N
13 eleq2 Ek=WNEkNW
14 elsni NWN=W
15 14 eqcomd NWW=N
16 13 15 syl6bi Ek=WNEkW=N
17 16 com12 NEkEk=WW=N
18 17 con3rr3 ¬W=NNEk¬Ek=W
19 12 18 sylbi WNNEk¬Ek=W
20 11 19 simplbiim WVNNEk¬Ek=W
21 20 com12 NEkWVN¬Ek=W
22 10 21 simplbiim kJWVN¬Ek=W
23 22 impcom WVNkJ¬Ek=W
24 23 ralrimiva WVNkJ¬Ek=W
25 rabeq0 kJ|Ek=W=kJ¬Ek=W
26 24 25 sylibr WVNkJ|Ek=W=
27 2 fvexi EV
28 27 dmex domEV
29 7 28 rab2ex kJ|Ek=WV
30 hasheq0 kJ|Ek=WVkJ|Ek=W=0kJ|Ek=W=
31 29 30 ax-mp kJ|Ek=W=0kJ|Ek=W=
32 26 31 sylibr WVNkJ|Ek=W=0