Metamath Proof Explorer


Theorem wlkp1lem7

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
wlkp1.q Q = P N + 1 C
wlkp1.s φ Vtx S = V
Assertion wlkp1lem7 φ Q N Q N + 1 iEdg S H N

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 wlkp1.q Q = P N + 1 C
15 wlkp1.s φ Vtx S = V
16 fveq2 k = N Q k = Q N
17 fveq2 k = N P k = P N
18 16 17 eqeq12d k = N Q k = P k Q N = P N
19 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem5 φ k 0 N Q k = P k
20 wlkcl F Walks G P F 0
21 9 eqcomi F = N
22 21 eleq1i F 0 N 0
23 nn0fz0 N 0 N 0 N
24 22 23 sylbb F 0 N 0 N
25 8 20 24 3syl φ N 0 N
26 18 19 25 rspcdva φ Q N = P N
27 14 fveq1i Q N + 1 = P N + 1 C N + 1
28 ovex N + 1 V
29 1 2 3 4 5 6 7 8 9 wlkp1lem1 φ ¬ N + 1 dom P
30 fsnunfv N + 1 V C V ¬ N + 1 dom P P N + 1 C N + 1 = C
31 28 6 29 30 mp3an2i φ P N + 1 C N + 1 = C
32 27 31 syl5eq φ Q N + 1 = C
33 26 32 preq12d φ Q N Q N + 1 = P N C
34 fsnunfv B W E Edg G ¬ B dom I I B E B = E
35 5 10 7 34 syl3anc φ I B E B = E
36 11 33 35 3sstr4d φ Q N Q N + 1 I B E B
37 1 2 3 4 5 6 7 8 9 10 11 12 13 wlkp1lem3 φ iEdg S H N = I B E B
38 36 37 sseqtrrd φ Q N Q N + 1 iEdg S H N