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

Theorem elwwlks2 28439
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 28388 . . 3 (𝑊 ∈ (2 WWalksN 𝐺) ↔ ∃𝑎𝑉𝑐𝑉 𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐))
32a1i 11 . 2 (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WWalksN 𝐺) ↔ ∃𝑎𝑉𝑐𝑉 𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)))
41elwwlks2on 28432 . . . 4 ((𝐺 ∈ UPGraph ∧ 𝑎𝑉𝑐𝑉) → (𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ∃𝑏𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2))))
543expb 1119 . . 3 ((𝐺 ∈ UPGraph ∧ (𝑎𝑉𝑐𝑉)) → (𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ∃𝑏𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2))))
652rexbidva 3208 . 2 (𝐺 ∈ UPGraph → (∃𝑎𝑉𝑐𝑉 𝑊 ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ∃𝑎𝑉𝑐𝑉𝑏𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2))))
7 rexcom 3270 . . . 4 (∃𝑐𝑉𝑏𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) ↔ ∃𝑏𝑉𝑐𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))
8 s3cli 14663 . . . . . . . . . 10 ⟨“𝑎𝑏𝑐”⟩ ∈ Word V
98a1i 11 . . . . . . . . 9 ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → ⟨“𝑎𝑏𝑐”⟩ ∈ Word V)
10 simplr 766 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → 𝑊 = ⟨“𝑎𝑏𝑐”⟩)
11 simpr 485 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → 𝑝 = ⟨“𝑎𝑏𝑐”⟩)
1210, 11eqtr4d 2780 . . . . . . . . . . . . . . . 16 (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → 𝑊 = 𝑝)
1312breq2d 5097 . . . . . . . . . . . . . . 15 (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (𝑓(Walks‘𝐺)𝑊𝑓(Walks‘𝐺)𝑝))
1413biimpd 228 . . . . . . . . . . . . . 14 (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (𝑓(Walks‘𝐺)𝑊𝑓(Walks‘𝐺)𝑝))
1514com12 32 . . . . . . . . . . . . 13 (𝑓(Walks‘𝐺)𝑊 → (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → 𝑓(Walks‘𝐺)𝑝))
1615adantr 481 . . . . . . . . . . . 12 ((𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2) → (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → 𝑓(Walks‘𝐺)𝑝))
1716impcom 408 . . . . . . . . . . 11 ((((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) → 𝑓(Walks‘𝐺)𝑝)
18 simprr 770 . . . . . . . . . . 11 ((((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) → (♯‘𝑓) = 2)
19 vex 3445 . . . . . . . . . . . . . . . 16 𝑎 ∈ V
20 s3fv0 14673 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ V → (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎)
2120eqcomd 2743 . . . . . . . . . . . . . . . 16 (𝑎 ∈ V → 𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0))
2219, 21mp1i 13 . . . . . . . . . . . . . . 15 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0))
23 fveq1 6808 . . . . . . . . . . . . . . 15 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑝‘0) = (⟨“𝑎𝑏𝑐”⟩‘0))
2422, 23eqtr4d 2780 . . . . . . . . . . . . . 14 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑎 = (𝑝‘0))
25 vex 3445 . . . . . . . . . . . . . . . 16 𝑏 ∈ V
26 s3fv1 14674 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ V → (⟨“𝑎𝑏𝑐”⟩‘1) = 𝑏)
2726eqcomd 2743 . . . . . . . . . . . . . . . 16 (𝑏 ∈ V → 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1))
2825, 27mp1i 13 . . . . . . . . . . . . . . 15 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1))
29 fveq1 6808 . . . . . . . . . . . . . . 15 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑝‘1) = (⟨“𝑎𝑏𝑐”⟩‘1))
3028, 29eqtr4d 2780 . . . . . . . . . . . . . 14 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑏 = (𝑝‘1))
31 vex 3445 . . . . . . . . . . . . . . . 16 𝑐 ∈ V
32 s3fv2 14675 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ V → (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)
3332eqcomd 2743 . . . . . . . . . . . . . . . 16 (𝑐 ∈ V → 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2))
3431, 33mp1i 13 . . . . . . . . . . . . . . 15 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2))
35 fveq1 6808 . . . . . . . . . . . . . . 15 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑝‘2) = (⟨“𝑎𝑏𝑐”⟩‘2))
3634, 35eqtr4d 2780 . . . . . . . . . . . . . 14 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑐 = (𝑝‘2))
3724, 30, 363jca 1127 . . . . . . . . . . . . 13 (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))
3837adantl 482 . . . . . . . . . . . 12 (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))
3938adantr 481 . . . . . . . . . . 11 ((((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) → (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))
4017, 18, 393jca 1127 . . . . . . . . . 10 ((((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) → (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))
4140ex 413 . . . . . . . . 9 (((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → ((𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2) → (𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
429, 41spcimedv 3543 . . . . . . . 8 ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → ((𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2) → ∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
43 wlklenvp1 28093 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓(Walks‘𝐺)𝑝 → (♯‘𝑝) = ((♯‘𝑓) + 1))
44 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((♯‘𝑝) = ((♯‘𝑓) + 1) ∧ (♯‘𝑓) = 2) → (♯‘𝑝) = ((♯‘𝑓) + 1))
45 oveq1 7320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((♯‘𝑓) = 2 → ((♯‘𝑓) + 1) = (2 + 1))
4645adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((♯‘𝑝) = ((♯‘𝑓) + 1) ∧ (♯‘𝑓) = 2) → ((♯‘𝑓) + 1) = (2 + 1))
4744, 46eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((♯‘𝑝) = ((♯‘𝑓) + 1) ∧ (♯‘𝑓) = 2) → (♯‘𝑝) = (2 + 1))
4847adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑝) = ((♯‘𝑓) + 1) ∧ (♯‘𝑓) = 2)) → (♯‘𝑝) = (2 + 1))
49 2p1e3 12185 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 + 1) = 3
5048, 49eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓(Walks‘𝐺)𝑝 ∧ ((♯‘𝑝) = ((♯‘𝑓) + 1) ∧ (♯‘𝑓) = 2)) → (♯‘𝑝) = 3)
5150exp32 421 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓(Walks‘𝐺)𝑝 → ((♯‘𝑝) = ((♯‘𝑓) + 1) → ((♯‘𝑓) = 2 → (♯‘𝑝) = 3)))
5243, 51mpd 15 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓(Walks‘𝐺)𝑝 → ((♯‘𝑓) = 2 → (♯‘𝑝) = 3))
5352adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) → ((♯‘𝑓) = 2 → (♯‘𝑝) = 3))
5453imp 407 . . . . . . . . . . . . . . . . . . . 20 (((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) → (♯‘𝑝) = 3)
55 eqcom 2744 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑝‘0) ↔ (𝑝‘0) = 𝑎)
5655biimpi 215 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑝‘0) → (𝑝‘0) = 𝑎)
57 eqcom 2744 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (𝑝‘1) ↔ (𝑝‘1) = 𝑏)
5857biimpi 215 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (𝑝‘1) → (𝑝‘1) = 𝑏)
59 eqcom 2744 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = (𝑝‘2) ↔ (𝑝‘2) = 𝑐)
6059biimpi 215 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = (𝑝‘2) → (𝑝‘2) = 𝑐)
6156, 58, 603anim123i 1150 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))
6254, 61anim12i 613 . . . . . . . . . . . . . . . . . . 19 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)))
631wlkpwrd 28092 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓(Walks‘𝐺)𝑝𝑝 ∈ Word 𝑉)
64 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐺 ∈ UPGraph ∧ 𝑎𝑉) → 𝑎𝑉)
6564anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) → (𝑎𝑉 ∧ (𝑏𝑉𝑐𝑉)))
66 3anass 1094 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎𝑉𝑏𝑉𝑐𝑉) ↔ (𝑎𝑉 ∧ (𝑏𝑉𝑐𝑉)))
6765, 66sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) → (𝑎𝑉𝑏𝑉𝑐𝑉))
6867adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (𝑎𝑉𝑏𝑉𝑐𝑉))
6963, 68anim12i 613 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) → (𝑝 ∈ Word 𝑉 ∧ (𝑎𝑉𝑏𝑉𝑐𝑉)))
7069ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑝 ∈ Word 𝑉 ∧ (𝑎𝑉𝑏𝑉𝑐𝑉)))
71 eqwrds3 14745 . . . . . . . . . . . . . . . . . . . 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 770 . . . . . . . . . . . . . . . . . . 19 ((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) → 𝑊 = ⟨“𝑎𝑏𝑐”⟩)
7574ad2antrr 723 . . . . . . . . . . . . . . . . . 18 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → 𝑊 = ⟨“𝑎𝑏𝑐”⟩)
7673, 75eqtr4d 2780 . . . . . . . . . . . . . . . . 17 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → 𝑝 = 𝑊)
7776breq2d 5097 . . . . . . . . . . . . . . . 16 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑝𝑓(Walks‘𝐺)𝑊))
7877biimpd 228 . . . . . . . . . . . . . . 15 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑝𝑓(Walks‘𝐺)𝑊))
79 simplr 766 . . . . . . . . . . . . . . 15 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (♯‘𝑓) = 2)
8078, 79jctird 527 . . . . . . . . . . . . . 14 ((((𝑓(Walks‘𝐺)𝑝 ∧ (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩)) ∧ (♯‘𝑓) = 2) ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑝 → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))
8180exp41 435 . . . . . . . . . . . . 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 1110 . . . . . . . . . 10 ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))
8584com12 32 . . . . . . . . 9 ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))
8685exlimdv 1935 . . . . . . . 8 ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)))
8742, 86impbid 211 . . . . . . 7 ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → ((𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2) ↔ ∃𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
8887exbidv 1923 . . . . . 6 ((((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2) ↔ ∃𝑓𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
8988pm5.32da 579 . . . . 5 (((𝐺 ∈ UPGraph ∧ 𝑎𝑉) ∧ (𝑏𝑉𝑐𝑉)) → ((𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) ↔ (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))
90892rexbidva 3208 . . . 4 ((𝐺 ∈ UPGraph ∧ 𝑎𝑉) → (∃𝑏𝑉𝑐𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) ↔ ∃𝑏𝑉𝑐𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))
917, 90bitrid 282 . . 3 ((𝐺 ∈ UPGraph ∧ 𝑎𝑉) → (∃𝑐𝑉𝑏𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓(𝑓(Walks‘𝐺)𝑊 ∧ (♯‘𝑓) = 2)) ↔ ∃𝑏𝑉𝑐𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓𝑝(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))
9291rexbidva 3170 . 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 396  w3a 1086   = wceq 1540  wex 1780  wcel 2105  wrex 3071  Vcvv 3441   class class class wbr 5085  cfv 6463  (class class class)co 7313  0cc0 10941  1c1 10942   + caddc 10944  2c2 12098  3c3 12099  chash 14114  Word cword 14286  ⟨“cs3 14624  Vtxcvtx 27474  UPGraphcupgr 27558  Walkscwlks 28071   WWalksN cwwlksn 28299   WWalksNOn cwwlksnon 28300
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5222  ax-sep 5236  ax-nul 5243  ax-pow 5301  ax-pr 5365  ax-un 7626  ax-ac2 10289  ax-cnex 10997  ax-resscn 10998  ax-1cn 10999  ax-icn 11000  ax-addcl 11001  ax-addrcl 11002  ax-mulcl 11003  ax-mulrcl 11004  ax-mulcom 11005  ax-addass 11006  ax-mulass 11007  ax-distr 11008  ax-i2m1 11009  ax-1ne0 11010  ax-1rid 11011  ax-rnegex 11012  ax-rrecex 11013  ax-cnre 11014  ax-pre-lttri 11015  ax-pre-lttrn 11016  ax-pre-ltadd 11017  ax-pre-mulgt0 11018
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ifp 1061  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4470  df-pw 4545  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4849  df-int 4891  df-iun 4937  df-br 5086  df-opab 5148  df-mpt 5169  df-tr 5203  df-id 5505  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5560  df-se 5561  df-we 5562  df-xp 5611  df-rel 5612  df-cnv 5613  df-co 5614  df-dm 5615  df-rn 5616  df-res 5617  df-ima 5618  df-pred 6222  df-ord 6289  df-on 6290  df-lim 6291  df-suc 6292  df-iota 6415  df-fun 6465  df-fn 6466  df-f 6467  df-f1 6468  df-fo 6469  df-f1o 6470  df-fv 6471  df-isom 6472  df-riota 7270  df-ov 7316  df-oprab 7317  df-mpo 7318  df-om 7756  df-1st 7874  df-2nd 7875  df-frecs 8142  df-wrecs 8173  df-recs 8247  df-rdg 8286  df-1o 8342  df-2o 8343  df-oadd 8346  df-er 8544  df-map 8663  df-pm 8664  df-en 8780  df-dom 8781  df-sdom 8782  df-fin 8783  df-dju 9727  df-card 9765  df-ac 9942  df-pnf 11081  df-mnf 11082  df-xr 11083  df-ltxr 11084  df-le 11085  df-sub 11277  df-neg 11278  df-nn 12044  df-2 12106  df-3 12107  df-n0 12304  df-xnn0 12376  df-z 12390  df-uz 12653  df-fz 13310  df-fzo 13453  df-hash 14115  df-word 14287  df-concat 14343  df-s1 14370  df-s2 14630  df-s3 14631  df-edg 27526  df-uhgr 27536  df-upgr 27560  df-wlks 28074  df-wwlks 28303  df-wwlksn 28304  df-wwlksnon 28305
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator