Metamath Proof Explorer


Theorem wlkp1lem3

Description: Lemma for wlkp1 . (Contributed by AV, 6-Mar-2021)

Ref Expression
Hypotheses wlkp1.v V=VtxG
wlkp1.i I=iEdgG
wlkp1.f φFunI
wlkp1.a φIFin
wlkp1.b φBW
wlkp1.c φCV
wlkp1.d φ¬BdomI
wlkp1.w φFWalksGP
wlkp1.n N=F
wlkp1.e φEEdgG
wlkp1.x φPNCE
wlkp1.u φiEdgS=IBE
wlkp1.h H=FNB
Assertion wlkp1lem3 φiEdgSHN=IBEB

Proof

Step Hyp Ref Expression
1 wlkp1.v V=VtxG
2 wlkp1.i I=iEdgG
3 wlkp1.f φFunI
4 wlkp1.a φIFin
5 wlkp1.b φBW
6 wlkp1.c φCV
7 wlkp1.d φ¬BdomI
8 wlkp1.w φFWalksGP
9 wlkp1.n N=F
10 wlkp1.e φEEdgG
11 wlkp1.x φPNCE
12 wlkp1.u φiEdgS=IBE
13 wlkp1.h H=FNB
14 13 a1i φH=FNB
15 14 fveq1d φHN=FNBN
16 9 fvexi NV
17 2 wlkf FWalksGPFWorddomI
18 lencl FWorddomIF0
19 wrddm FWorddomIdomF=0..^F
20 fzonel ¬F0..^F
21 9 a1i F0domF=0..^FN=F
22 simpr F0domF=0..^FdomF=0..^F
23 21 22 eleq12d F0domF=0..^FNdomFF0..^F
24 20 23 mtbiri F0domF=0..^F¬NdomF
25 18 19 24 syl2anc FWorddomI¬NdomF
26 8 17 25 3syl φ¬NdomF
27 fsnunfv NVBW¬NdomFFNBN=B
28 16 5 26 27 mp3an2i φFNBN=B
29 15 28 eqtrd φHN=B
30 12 29 fveq12d φiEdgSHN=IBEB