MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elwwlks2 Structured version   Visualization version   GIF version

Theorem elwwlks2 29849
Description: A walk of length 2 between two vertices as length 3 string in a pseudograph. (Contributed by Alexander van der Vekens, 21-Feb-2018.) (Revised by AV, 17-May-2021.) (Proof shortened by AV, 14-Mar-2022.)
Hypothesis
Ref Expression
elwwlks2.v 𝑉 = (Vtx‘𝐺)
Assertion
Ref Expression
elwwlks2 (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WWalksN 𝐺) ↔ ∃𝑎𝑉𝑏𝑉𝑐𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))
Distinct variable groups:   𝐺,𝑎,𝑏,𝑐,𝑓,𝑝   𝑉,𝑎,𝑏,𝑐,𝑓,𝑝   𝑊,𝑎,𝑏,𝑐,𝑓,𝑝

Proof of Theorem elwwlks2
StepHypRef Expression
1 elwwlks2.v . . . 4 𝑉 = (Vtx‘𝐺)
21wwlksnwwlksnon 29798 . . 3 (𝑊 ∈ (2 WWalksN 𝐺) ↔ ∃𝑎𝑉𝑐𝑉 𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐))
32a1i 11 . 2 (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WWalksN 𝐺) ↔ ∃𝑎𝑉𝑐𝑉 𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)))
41elwwlks2on 29842 . . . 4 ((𝐺 ∈ UPGraph ∧ 𝑎𝑉𝑐𝑉) → (𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ∃𝑏𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2))))
543expb 1117 . . 3 ((𝐺 ∈ UPGraph ∧ (𝑎𝑉𝑐𝑉)) → (𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ∃𝑏𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2))))
652rexbidva 3207 . 2 (𝐺 ∈ UPGraph → (∃𝑎𝑉𝑐𝑉 𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ∃𝑎𝑉𝑐𝑉𝑏𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2))))
7 rexcom 3277 . . . 4 (∃𝑐𝑉𝑏𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) ↔ ∃𝑏𝑉𝑐𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))
8 s3cli 14868 . . . . . . . . . 10 ⟨“𝑎𝑏𝑐”⟩ ∈ Word V
98a1i 11 . . . . . . . . 9 ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → ⟨“𝑎𝑏𝑐”⟩ ∈ Word V)
10 simplr 767 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → 𝑊 = ⟨“𝑎𝑏𝑐”⟩)
11 simpr 483 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → 𝑝 = ⟨“𝑎𝑏𝑐”⟩)
1210, 11eqtr4d 2768 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → 𝑊 = 𝑝)
1312breq2d 5161 . . . . . . . . . . . . . . 15 (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (𝑓(Walks‘𝐺)𝑊𝑓(Walks‘𝐺)𝑝))
1413biimpd 228 . . . . . . . . . . . . . 14 (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (𝑓(Walks‘𝐺)𝑊𝑓(Walks‘𝐺)𝑝))
1514com12 32 . . . . . . . . . . . . 13 (𝑓(Walks‘𝐺)𝑊 → (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → 𝑓(Walks‘𝐺)𝑝))
1615adantr 479 . . . . . . . . . . . 12 ((𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2) → (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → 𝑓(Walks‘𝐺)𝑝))
1716impcom 406 . . . . . . . . . . 11 ((((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) → 𝑓(Walks‘𝐺)𝑝)
18 simprr 771 . . . . . . . . . . 11 ((((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) → (♯‘𝑓) = 2)
19 vex 3465 . . . . . . . . . . . . . . . 16 𝑎 ∈ V
20 s3fv0 14878 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ V → (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎)
2120eqcomd 2731 . . . . . . . . . . . . . . . 16 (𝑎 ∈ V → 𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0))
2219, 21mp1i 13 . . . . . . . . . . . . . . 15 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0))
23 fveq1 6895 . . . . . . . . . . . . . . 15 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑝‘0) = (⟨“𝑎𝑏𝑐”⟩‘0))
2422, 23eqtr4d 2768 . . . . . . . . . . . . . 14 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑎 = (𝑝‘0))
25 vex 3465 . . . . . . . . . . . . . . . 16 𝑏 ∈ V
26 s3fv1 14879 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ V → (⟨“𝑎𝑏𝑐”⟩‘1) = 𝑏)
2726eqcomd 2731 . . . . . . . . . . . . . . . 16 (𝑏 ∈ V → 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1))
2825, 27mp1i 13 . . . . . . . . . . . . . . 15 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1))
29 fveq1 6895 . . . . . . . . . . . . . . 15 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑝‘1) = (⟨“𝑎𝑏𝑐”⟩‘1))
3028, 29eqtr4d 2768 . . . . . . . . . . . . . 14 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑏 = (𝑝‘1))
31 vex 3465 . . . . . . . . . . . . . . . 16 𝑐 ∈ V
32 s3fv2 14880 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ V → (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)
3332eqcomd 2731 . . . . . . . . . . . . . . . 16 (𝑐 ∈ V → 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2))
3431, 33mp1i 13 . . . . . . . . . . . . . . 15 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2))
35 fveq1 6895 . . . . . . . . . . . . . . 15 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑝‘2) = (⟨“𝑎𝑏𝑐”⟩‘2))
3634, 35eqtr4d 2768 . . . . . . . . . . . . . 14 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑐 = (𝑝‘2))
3724, 30, 363jca 1125 . . . . . . . . . . . . 13 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))
3837adantl 480 . . . . . . . . . . . 12 (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))
3938adantr 479 . . . . . . . . . . 11 ((((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) → (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))
4017, 18, 393jca 1125 . . . . . . . . . 10 ((((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) → (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))
4140ex 411 . . . . . . . . 9 (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → ((𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2) → (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
429, 41spcimedv 3579 . . . . . . . 8 ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → ((𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2) → ∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
43 wlklenvp1 29504 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓(Walks‘𝐺)𝑝 → (♯‘𝑝) = ((♯‘𝑓) + 1))
44 simpl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((♯‘𝑝) = ((♯‘𝑓) + 1) ∧ (♯‘𝑓) = 2) → (♯‘𝑝) = ((♯‘𝑓) + 1))
45 oveq1 7426 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((♯‘𝑓) = 2 → ((♯‘𝑓) + 1) = (2 + 1))
4645adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((♯‘𝑝) = ((♯‘𝑓) + 1) ∧ (♯‘𝑓) = 2) → ((♯‘𝑓) + 1) = (2 + 1))
4744, 46eqtrd 2765 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((♯‘𝑝) = ((♯‘𝑓) + 1) ∧ (♯‘𝑓) = 2) → (♯‘𝑝) = (2 + 1))
4847adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑝) = ((♯‘𝑓) + 1) ∧ (♯‘𝑓) = 2)) → (♯‘𝑝) = (2 + 1))
49 2p1e3 12387 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 + 1) = 3
5048, 49eqtrdi 2781 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑝) = ((♯‘𝑓) + 1) ∧ (♯‘𝑓) = 2)) → (♯‘𝑝) = 3)
5150exp32 419 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓(Walks‘𝐺)𝑝 → ((♯‘𝑝) = ((♯‘𝑓) + 1) → ((♯‘𝑓) = 2 → (♯‘𝑝) = 3)))
5243, 51mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓(Walks‘𝐺)𝑝 → ((♯‘𝑓) = 2 → (♯‘𝑝) = 3))
5352adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) → ((♯‘𝑓) = 2 → (♯‘𝑝) = 3))
5453imp 405 . . . . . . . . . . . . . . . . . . . 20 (((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) → (♯‘𝑝) = 3)
55 eqcom 2732 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑝‘0) ↔ (𝑝‘0) = 𝑎)
5655biimpi 215 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑝‘0) → (𝑝‘0) = 𝑎)
57 eqcom 2732 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑝‘1) ↔ (𝑝‘1) = 𝑏)
5857biimpi 215 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑝‘1) → (𝑝‘1) = 𝑏)
59 eqcom 2732 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = (𝑝‘2) ↔ (𝑝‘2) = 𝑐)
6059biimpi 215 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = (𝑝‘2) → (𝑝‘2) = 𝑐)
6156, 58, 603anim123i 1148 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))
6254, 61anim12i 611 . . . . . . . . . . . . . . . . . . 19 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)))
631wlkpwrd 29503 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓(Walks‘𝐺)𝑝𝑝 ∈ Word 𝑉)
64 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ UPGraph ∧ 𝑎𝑉) → 𝑎𝑉)
6564anim1i 613 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) → (𝑎𝑉 ∧ (𝑏𝑉𝑐𝑉)))
66 3anass 1092 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝑉𝑏𝑉𝑐𝑉) ↔ (𝑎𝑉 ∧ (𝑏𝑉𝑐𝑉)))
6765, 66sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) → (𝑎𝑉𝑏𝑉𝑐𝑉))
6867adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (𝑎𝑉𝑏𝑉𝑐𝑉))
6963, 68anim12i 611 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) → (𝑝 ∈ Word 𝑉 ∧ (𝑎𝑉𝑏𝑉𝑐𝑉)))
7069ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑝 ∈ Word 𝑉 ∧ (𝑎𝑉𝑏𝑉𝑐𝑉)))
71 eqwrds3 14948 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ Word 𝑉 ∧ (𝑎𝑉𝑏𝑉𝑐𝑉)) → (𝑝 = ⟨“𝑎𝑏𝑐”⟩ ↔ ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))))
7270, 71syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑝 = ⟨“𝑎𝑏𝑐”⟩ ↔ ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))))
7362, 72mpbird 256 . . . . . . . . . . . . . . . . . 18 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → 𝑝 = ⟨“𝑎𝑏𝑐”⟩)
74 simprr 771 . . . . . . . . . . . . . . . . . . 19 ((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) → 𝑊 = ⟨“𝑎𝑏𝑐”⟩)
7574ad2antrr 724 . . . . . . . . . . . . . . . . . 18 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → 𝑊 = ⟨“𝑎𝑏𝑐”⟩)
7673, 75eqtr4d 2768 . . . . . . . . . . . . . . . . 17 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → 𝑝 = 𝑊)
7776breq2d 5161 . . . . . . . . . . . . . . . 16 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑝𝑓(Walks‘𝐺)𝑊))
7877biimpd 228 . . . . . . . . . . . . . . 15 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑝𝑓(Walks‘𝐺)𝑊))
79 simplr 767 . . . . . . . . . . . . . . 15 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (♯‘𝑓) = 2)
8078, 79jctird 525 . . . . . . . . . . . . . 14 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑝 → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))
8180exp41 433 . . . . . . . . . . . . 13 (𝑓(Walks‘𝐺)𝑝 → ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → ((♯‘𝑓) = 2 → ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → (𝑓(Walks‘𝐺)𝑝 → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2))))))
8281com25 99 . . . . . . . . . . . 12 (𝑓(Walks‘𝐺)𝑝 → (𝑓(Walks‘𝐺)𝑝 → ((♯‘𝑓) = 2 → ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2))))))
8382pm2.43i 52 . . . . . . . . . . 11 (𝑓(Walks‘𝐺)𝑝 → ((♯‘𝑓) = 2 → ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))))
84833imp 1108 . . . . . . . . . 10 ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))
8584com12 32 . . . . . . . . 9 ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))
8685exlimdv 1928 . . . . . . . 8 ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))
8742, 86impbid 211 . . . . . . 7 ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → ((𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2) ↔ ∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
8887exbidv 1916 . . . . . 6 ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2) ↔ ∃𝑓𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
8988pm5.32da 577 . . . . 5 (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) → ((𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) ↔ (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))
90892rexbidva 3207 . . . 4 ((𝐺 ∈ UPGraph ∧ 𝑎𝑉) → (∃𝑏𝑉𝑐𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) ↔ ∃𝑏𝑉𝑐𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))
917, 90bitrid 282 . . 3 ((𝐺 ∈ UPGraph ∧ 𝑎𝑉) → (∃𝑐𝑉𝑏𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) ↔ ∃𝑏𝑉𝑐𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))
9291rexbidva 3166 . 2 (𝐺 ∈ UPGraph → (∃𝑎𝑉𝑐𝑉𝑏𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) ↔ ∃𝑎𝑉𝑏𝑉𝑐𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))
933, 6, 923bitrd 304 1 (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WWalksN 𝐺) ↔ ∃𝑎𝑉𝑏𝑉𝑐𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wex 1773  wcel 2098  wrex 3059  Vcvv 3461   class class class wbr 5149  cfv 6549  (class class class)co 7419  0cc0 11140  1c1 11141   + caddc 11143  2c2 12300  3c3 12301  chash 14325  Word cword 14500  ⟨“cs3 14829  Vtxcvtx 28881  UPGraphcupgr 28965  Walkscwlks 29482   WWalksN cwwlksn 29709   WWalksNOn cwwlksnon 29710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-ac2 10488  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ifp 1061  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-oadd 8491  df-er 8725  df-map 8847  df-pm 8848  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-dju 9926  df-card 9964  df-ac 10141  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-nn 12246  df-2 12308  df-3 12309  df-n0 12506  df-xnn0 12578  df-z 12592  df-uz 12856  df-fz 13520  df-fzo 13663  df-hash 14326  df-word 14501  df-concat 14557  df-s1 14582  df-s2 14835  df-s3 14836  df-edg 28933  df-uhgr 28943  df-upgr 28967  df-wlks 29485  df-wwlks 29713  df-wwlksn 29714  df-wwlksnon 29715
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator