Metamath Proof Explorer


Theorem usgr2wlkspthlem2

Description: Lemma 2 for usgr2wlkspth . (Contributed by Alexander van der Vekens, 2-Mar-2018) (Revised by AV, 27-Jan-2021)

Ref Expression
Assertion usgr2wlkspthlem2 F Walks G P G USGraph F = 2 P 0 P F Fun P -1

Proof

Step Hyp Ref Expression
1 simp1 G USGraph F = 2 P 0 P F G USGraph
2 1 anim2i F Walks G P G USGraph F = 2 P 0 P F F Walks G P G USGraph
3 2 ancomd F Walks G P G USGraph F = 2 P 0 P F G USGraph F Walks G P
4 3simpc G USGraph F = 2 P 0 P F F = 2 P 0 P F
5 4 adantl F Walks G P G USGraph F = 2 P 0 P F F = 2 P 0 P F
6 usgr2wlkneq G USGraph F Walks G P F = 2 P 0 P F P 0 P 1 P 0 P 2 P 1 P 2 F 0 F 1
7 3 5 6 syl2anc F Walks G P G USGraph F = 2 P 0 P F P 0 P 1 P 0 P 2 P 1 P 2 F 0 F 1
8 simpl P 0 P 1 P 0 P 2 P 1 P 2 F 0 F 1 P 0 P 1 P 0 P 2 P 1 P 2
9 fvex P 0 V
10 fvex P 1 V
11 fvex P 2 V
12 9 10 11 3pm3.2i P 0 V P 1 V P 2 V
13 8 12 jctil P 0 P 1 P 0 P 2 P 1 P 2 F 0 F 1 P 0 V P 1 V P 2 V P 0 P 1 P 0 P 2 P 1 P 2
14 funcnvs3 P 0 V P 1 V P 2 V P 0 P 1 P 0 P 2 P 1 P 2 Fun ⟨“ P 0 P 1 P 2 ”⟩ -1
15 7 13 14 3syl F Walks G P G USGraph F = 2 P 0 P F Fun ⟨“ P 0 P 1 P 2 ”⟩ -1
16 eqid Vtx G = Vtx G
17 16 wlkpwrd F Walks G P P Word Vtx G
18 wlklenvp1 F Walks G P P = F + 1
19 oveq1 F = 2 F + 1 = 2 + 1
20 2p1e3 2 + 1 = 3
21 19 20 eqtrdi F = 2 F + 1 = 3
22 21 3ad2ant2 G USGraph F = 2 P 0 P F F + 1 = 3
23 18 22 sylan9eq F Walks G P G USGraph F = 2 P 0 P F P = 3
24 wrdlen3s3 P Word Vtx G P = 3 P = ⟨“ P 0 P 1 P 2 ”⟩
25 17 23 24 syl2an2r F Walks G P G USGraph F = 2 P 0 P F P = ⟨“ P 0 P 1 P 2 ”⟩
26 25 cnveqd F Walks G P G USGraph F = 2 P 0 P F P -1 = ⟨“ P 0 P 1 P 2 ”⟩ -1
27 26 funeqd F Walks G P G USGraph F = 2 P 0 P F Fun P -1 Fun ⟨“ P 0 P 1 P 2 ”⟩ -1
28 15 27 mpbird F Walks G P G USGraph F = 2 P 0 P F Fun P -1