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

Theorem wpthswwlks2on 27164
Description: For two different vertices, a walk of length 2 between these vertices is a simple path of length 2 between these vertices in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 13-May-2021.) (Revised by AV, 16-Mar-2022.)
Assertion
Ref Expression
wpthswwlks2on ((𝐺 ∈ USGraph ∧ 𝐴𝐵) → (𝐴(2 WSPathsNOn 𝐺)𝐵) = (𝐴(2 WWalksNOn 𝐺)𝐵))

Proof of Theorem wpthswwlks2on
Dummy variables 𝑓 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wwlknon 27043 . . . . . . 7 (𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ (𝑤 ∈ (2 WWalksN 𝐺) ∧ (𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵))
21a1i 11 . . . . . 6 ((𝐺 ∈ USGraph ∧ 𝐴𝐵) → (𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ↔ (𝑤 ∈ (2 WWalksN 𝐺) ∧ (𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)))
32anbi1d 623 . . . . 5 ((𝐺 ∈ USGraph ∧ 𝐴𝐵) → ((𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤) ↔ ((𝑤 ∈ (2 WWalksN 𝐺) ∧ (𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤)))
4 3anass 1116 . . . . . . 7 ((𝑤 ∈ (2 WWalksN 𝐺) ∧ (𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) ↔ (𝑤 ∈ (2 WWalksN 𝐺) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)))
54anbi1i 617 . . . . . 6 (((𝑤 ∈ (2 WWalksN 𝐺) ∧ (𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤) ↔ ((𝑤 ∈ (2 WWalksN 𝐺) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤))
6 anass 460 . . . . . 6 (((𝑤 ∈ (2 WWalksN 𝐺) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤) ↔ (𝑤 ∈ (2 WWalksN 𝐺) ∧ (((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤)))
75, 6bitri 266 . . . . 5 (((𝑤 ∈ (2 WWalksN 𝐺) ∧ (𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤) ↔ (𝑤 ∈ (2 WWalksN 𝐺) ∧ (((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤)))
83, 7syl6bb 278 . . . 4 ((𝐺 ∈ USGraph ∧ 𝐴𝐵) → ((𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤) ↔ (𝑤 ∈ (2 WWalksN 𝐺) ∧ (((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤))))
98rabbidva2 3334 . . 3 ((𝐺 ∈ USGraph ∧ 𝐴𝐵) → {𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤} = {𝑤 ∈ (2 WWalksN 𝐺) ∣ (((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤)})
10 usgrupgr 26354 . . . . . . . . . . 11 (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph)
11 wlklnwwlknupgr 27075 . . . . . . . . . . 11 (𝐺 ∈ UPGraph → (∃𝑓(𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2) ↔ 𝑤 ∈ (2 WWalksN 𝐺)))
1210, 11syl 17 . . . . . . . . . 10 (𝐺 ∈ USGraph → (∃𝑓(𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2) ↔ 𝑤 ∈ (2 WWalksN 𝐺)))
1312bicomd 214 . . . . . . . . 9 (𝐺 ∈ USGraph → (𝑤 ∈ (2 WWalksN 𝐺) ↔ ∃𝑓(𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2)))
1413adantr 472 . . . . . . . 8 ((𝐺 ∈ USGraph ∧ 𝐴𝐵) → (𝑤 ∈ (2 WWalksN 𝐺) ↔ ∃𝑓(𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2)))
15 simprl 787 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) ∧ (𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2)) → 𝑓(Walks‘𝐺)𝑤)
16 simprl 787 . . . . . . . . . . . . . . 15 (((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) → (𝑤‘0) = 𝐴)
1716adantr 472 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) ∧ (𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2)) → (𝑤‘0) = 𝐴)
18 fveq2 6374 . . . . . . . . . . . . . . . 16 ((♯‘𝑓) = 2 → (𝑤‘(♯‘𝑓)) = (𝑤‘2))
1918ad2antll 720 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) ∧ (𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2)) → (𝑤‘(♯‘𝑓)) = (𝑤‘2))
20 simprr 789 . . . . . . . . . . . . . . . 16 (((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) → (𝑤‘2) = 𝐵)
2120adantr 472 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) ∧ (𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2)) → (𝑤‘2) = 𝐵)
2219, 21eqtrd 2798 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) ∧ (𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2)) → (𝑤‘(♯‘𝑓)) = 𝐵)
23 eqid 2764 . . . . . . . . . . . . . . . . . . . . . 22 (Vtx‘𝐺) = (Vtx‘𝐺)
2423wlkp 26802 . . . . . . . . . . . . . . . . . . . . 21 (𝑓(Walks‘𝐺)𝑤𝑤:(0...(♯‘𝑓))⟶(Vtx‘𝐺))
25 oveq2 6849 . . . . . . . . . . . . . . . . . . . . . 22 ((♯‘𝑓) = 2 → (0...(♯‘𝑓)) = (0...2))
2625feq2d 6208 . . . . . . . . . . . . . . . . . . . . 21 ((♯‘𝑓) = 2 → (𝑤:(0...(♯‘𝑓))⟶(Vtx‘𝐺) ↔ 𝑤:(0...2)⟶(Vtx‘𝐺)))
2724, 26syl5ibcom 236 . . . . . . . . . . . . . . . . . . . 20 (𝑓(Walks‘𝐺)𝑤 → ((♯‘𝑓) = 2 → 𝑤:(0...2)⟶(Vtx‘𝐺)))
2827imp 395 . . . . . . . . . . . . . . . . . . 19 ((𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2) → 𝑤:(0...2)⟶(Vtx‘𝐺))
29 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑤:(0...2)⟶(Vtx‘𝐺) → 𝑤:(0...2)⟶(Vtx‘𝐺))
30 2nn0 11556 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℕ0
31 0elfz 12643 . . . . . . . . . . . . . . . . . . . . . 22 (2 ∈ ℕ0 → 0 ∈ (0...2))
3230, 31mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 (𝑤:(0...2)⟶(Vtx‘𝐺) → 0 ∈ (0...2))
3329, 32ffvelrnd 6549 . . . . . . . . . . . . . . . . . . . 20 (𝑤:(0...2)⟶(Vtx‘𝐺) → (𝑤‘0) ∈ (Vtx‘𝐺))
34 nn0fz0 12644 . . . . . . . . . . . . . . . . . . . . . . 23 (2 ∈ ℕ0 ↔ 2 ∈ (0...2))
3530, 34mpbi 221 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ (0...2)
3635a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑤:(0...2)⟶(Vtx‘𝐺) → 2 ∈ (0...2))
3729, 36ffvelrnd 6549 . . . . . . . . . . . . . . . . . . . 20 (𝑤:(0...2)⟶(Vtx‘𝐺) → (𝑤‘2) ∈ (Vtx‘𝐺))
3833, 37jca 507 . . . . . . . . . . . . . . . . . . 19 (𝑤:(0...2)⟶(Vtx‘𝐺) → ((𝑤‘0) ∈ (Vtx‘𝐺) ∧ (𝑤‘2) ∈ (Vtx‘𝐺)))
3928, 38syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2) → ((𝑤‘0) ∈ (Vtx‘𝐺) ∧ (𝑤‘2) ∈ (Vtx‘𝐺)))
40 eleq1 2831 . . . . . . . . . . . . . . . . . . 19 ((𝑤‘0) = 𝐴 → ((𝑤‘0) ∈ (Vtx‘𝐺) ↔ 𝐴 ∈ (Vtx‘𝐺)))
41 eleq1 2831 . . . . . . . . . . . . . . . . . . 19 ((𝑤‘2) = 𝐵 → ((𝑤‘2) ∈ (Vtx‘𝐺) ↔ 𝐵 ∈ (Vtx‘𝐺)))
4240, 41bi2anan9 629 . . . . . . . . . . . . . . . . . 18 (((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) → (((𝑤‘0) ∈ (Vtx‘𝐺) ∧ (𝑤‘2) ∈ (Vtx‘𝐺)) ↔ (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))))
4339, 42syl5ib 235 . . . . . . . . . . . . . . . . 17 (((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) → ((𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))))
4443adantl 473 . . . . . . . . . . . . . . . 16 (((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) → ((𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺))))
4544imp 395 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) ∧ (𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2)) → (𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)))
46 vex 3352 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
47 vex 3352 . . . . . . . . . . . . . . . 16 𝑤 ∈ V
4846, 47pm3.2i 462 . . . . . . . . . . . . . . 15 (𝑓 ∈ V ∧ 𝑤 ∈ V)
4923iswlkon 26843 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝑓 ∈ V ∧ 𝑤 ∈ V)) → (𝑓(𝐴(WalksOn‘𝐺)𝐵)𝑤 ↔ (𝑓(Walks‘𝐺)𝑤 ∧ (𝑤‘0) = 𝐴 ∧ (𝑤‘(♯‘𝑓)) = 𝐵)))
5045, 48, 49sylancl 580 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) ∧ (𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2)) → (𝑓(𝐴(WalksOn‘𝐺)𝐵)𝑤 ↔ (𝑓(Walks‘𝐺)𝑤 ∧ (𝑤‘0) = 𝐴 ∧ (𝑤‘(♯‘𝑓)) = 𝐵)))
5115, 17, 22, 50mpbir3and 1442 . . . . . . . . . . . . 13 ((((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) ∧ (𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2)) → 𝑓(𝐴(WalksOn‘𝐺)𝐵)𝑤)
52 simplll 791 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) ∧ (𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2)) → 𝐺 ∈ USGraph)
53 simprr 789 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) ∧ (𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2)) → (♯‘𝑓) = 2)
54 simpllr 793 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) ∧ (𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2)) → 𝐴𝐵)
55 usgr2wlkspth 26945 . . . . . . . . . . . . . 14 ((𝐺 ∈ USGraph ∧ (♯‘𝑓) = 2 ∧ 𝐴𝐵) → (𝑓(𝐴(WalksOn‘𝐺)𝐵)𝑤𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤))
5652, 53, 54, 55syl3anc 1490 . . . . . . . . . . . . 13 ((((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) ∧ (𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2)) → (𝑓(𝐴(WalksOn‘𝐺)𝐵)𝑤𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤))
5751, 56mpbid 223 . . . . . . . . . . . 12 ((((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) ∧ (𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2)) → 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤)
5857ex 401 . . . . . . . . . . 11 (((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) → ((𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2) → 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤))
5958eximdv 2012 . . . . . . . . . 10 (((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)) → (∃𝑓(𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2) → ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤))
6059ex 401 . . . . . . . . 9 ((𝐺 ∈ USGraph ∧ 𝐴𝐵) → (((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) → (∃𝑓(𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2) → ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤)))
6160com23 86 . . . . . . . 8 ((𝐺 ∈ USGraph ∧ 𝐴𝐵) → (∃𝑓(𝑓(Walks‘𝐺)𝑤 ∧ (♯‘𝑓) = 2) → (((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) → ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤)))
6214, 61sylbid 231 . . . . . . 7 ((𝐺 ∈ USGraph ∧ 𝐴𝐵) → (𝑤 ∈ (2 WWalksN 𝐺) → (((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) → ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤)))
6362imp 395 . . . . . 6 (((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ 𝑤 ∈ (2 WWalksN 𝐺)) → (((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) → ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤))
6463pm4.71d 557 . . . . 5 (((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ 𝑤 ∈ (2 WWalksN 𝐺)) → (((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) ↔ (((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤)))
6564bicomd 214 . . . 4 (((𝐺 ∈ USGraph ∧ 𝐴𝐵) ∧ 𝑤 ∈ (2 WWalksN 𝐺)) → ((((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤) ↔ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)))
6665rabbidva 3336 . . 3 ((𝐺 ∈ USGraph ∧ 𝐴𝐵) → {𝑤 ∈ (2 WWalksN 𝐺) ∣ (((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤)} = {𝑤 ∈ (2 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)})
679, 66eqtrd 2798 . 2 ((𝐺 ∈ USGraph ∧ 𝐴𝐵) → {𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤} = {𝑤 ∈ (2 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)})
6823iswspthsnon 27041 . 2 (𝐴(2 WSPathsNOn 𝐺)𝐵) = {𝑤 ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤}
6923iswwlksnon 27037 . 2 (𝐴(2 WWalksNOn 𝐺)𝐵) = {𝑤 ∈ (2 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘2) = 𝐵)}
7067, 68, 693eqtr4g 2823 1 ((𝐺 ∈ USGraph ∧ 𝐴𝐵) → (𝐴(2 WSPathsNOn 𝐺)𝐵) = (𝐴(2 WWalksNOn 𝐺)𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wex 1874  wcel 2155  wne 2936  {crab 3058  Vcvv 3349   class class class wbr 4808  wf 6063  cfv 6067  (class class class)co 6841  0cc0 10188  2c2 11326  0cn0 11537  ...cfz 12532  chash 13320  Vtxcvtx 26164  UPGraphcupgr 26251  USGraphcusgr 26321  Walkscwlks 26782  WalksOncwlkson 26783  SPathsOncspthson 26901   WWalksN cwwlksn 27009   WWalksNOn cwwlksnon 27010   WSPathsNOn cwwspthsnon 27012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-ac2 9537  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-ifp 1086  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-om 7263  df-1st 7365  df-2nd 7366  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-2o 7764  df-oadd 7767  df-er 7946  df-map 8061  df-pm 8062  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-card 9015  df-ac 9189  df-cda 9242  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-nn 11274  df-2 11334  df-3 11335  df-n0 11538  df-xnn0 11610  df-z 11624  df-uz 11886  df-fz 12533  df-fzo 12673  df-hash 13321  df-word 13486  df-concat 13541  df-s1 13566  df-s2 13878  df-s3 13879  df-edg 26216  df-uhgr 26229  df-upgr 26253  df-umgr 26254  df-uspgr 26322  df-usgr 26323  df-wlks 26785  df-wlkson 26786  df-trls 26879  df-trlson 26880  df-pths 26902  df-spths 26903  df-pthson 26904  df-spthson 26905  df-wwlks 27013  df-wwlksn 27014  df-wwlksnon 27015  df-wspthsnon 27017
This theorem is referenced by:  usgr2wspthons3  27168  frgr2wsp1  27567
  Copyright terms: Public domain W3C validator