Metamath Proof Explorer


Theorem wlkp1lem3

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

Ref Expression
Hypotheses wlkp1.v V = Vtx G
wlkp1.i I = iEdg G
wlkp1.f φ Fun I
wlkp1.a φ I Fin
wlkp1.b φ B W
wlkp1.c φ C V
wlkp1.d φ ¬ B dom I
wlkp1.w φ F Walks G P
wlkp1.n N = F
wlkp1.e φ E Edg G
wlkp1.x φ P N C E
wlkp1.u φ iEdg S = I B E
wlkp1.h H = F N B
Assertion wlkp1lem3 φ iEdg S H N = I B E B

Proof

Step Hyp Ref Expression
1 wlkp1.v V = Vtx G
2 wlkp1.i I = iEdg G
3 wlkp1.f φ Fun I
4 wlkp1.a φ I Fin
5 wlkp1.b φ B W
6 wlkp1.c φ C V
7 wlkp1.d φ ¬ B dom I
8 wlkp1.w φ F Walks G P
9 wlkp1.n N = F
10 wlkp1.e φ E Edg G
11 wlkp1.x φ P N C E
12 wlkp1.u φ iEdg S = I B E
13 wlkp1.h H = F N B
14 13 a1i φ H = F N B
15 14 fveq1d φ H N = F N B N
16 9 fvexi N V
17 2 wlkf F Walks G P F Word dom I
18 lencl F Word dom I F 0
19 wrddm F Word dom I dom F = 0 ..^ F
20 fzonel ¬ F 0 ..^ F
21 9 a1i F 0 dom F = 0 ..^ F N = F
22 simpr F 0 dom F = 0 ..^ F dom F = 0 ..^ F
23 21 22 eleq12d F 0 dom F = 0 ..^ F N dom F F 0 ..^ F
24 20 23 mtbiri F 0 dom F = 0 ..^ F ¬ N dom F
25 18 19 24 syl2anc F Word dom I ¬ N dom F
26 8 17 25 3syl φ ¬ N dom F
27 fsnunfv N V B W ¬ N dom F F N B N = B
28 16 5 26 27 mp3an2i φ F N B N = B
29 15 28 eqtrd φ H N = B
30 12 29 fveq12d φ iEdg S H N = I B E B