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

Theorem fusgr2wsp2nb 27537
Description: The set of paths of length 2 with a given vertex in the middle for a finite simple graph is the union of all paths of length 2 from one neighbor to another neighbor of this vertex via this vertex. (Contributed by Alexander van der Vekens, 9-Mar-2018.) (Revised by AV, 17-May-2021.) (Proof shortened by AV, 16-Mar-2022.)
Hypotheses
Ref Expression
frgrhash2wsp.v 𝑉 = (Vtx‘𝐺)
fusgreg2wsp.m 𝑀 = (𝑎𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})
Assertion
Ref Expression
fusgr2wsp2nb ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑀𝑁) = 𝑥 ∈ (𝐺 NeighbVtx 𝑁) 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){⟨“𝑥𝑁𝑦”⟩})
Distinct variable groups:   𝐺,𝑎   𝑉,𝑎   𝑤,𝐺   𝑁,𝑎,𝑤   𝑥,𝐺,𝑦   𝑥,𝑁,𝑦   𝑥,𝑉,𝑦
Allowed substitution hints:   𝑀(𝑥,𝑦,𝑤,𝑎)   𝑉(𝑤)

Proof of Theorem fusgr2wsp2nb
Dummy variables 𝑚 𝑧 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frgrhash2wsp.v . . . . . 6 𝑉 = (Vtx‘𝐺)
2 fusgreg2wsp.m . . . . . 6 𝑀 = (𝑎𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})
31, 2fusgreg2wsplem 27536 . . . . 5 (𝑁𝑉 → (𝑧 ∈ (𝑀𝑁) ↔ (𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁)))
43adantl 468 . . . 4 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (𝑀𝑁) ↔ (𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁)))
51wspthsnwspthsnon 27082 . . . . . . 7 (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥𝑉𝑦𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦))
6 fusgrusgr 26458 . . . . . . . . . 10 (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph)
76adantr 467 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → 𝐺 ∈ USGraph)
8 eqid 2774 . . . . . . . . . 10 (Edg‘𝐺) = (Edg‘𝐺)
91, 8usgr2wspthon 27135 . . . . . . . . 9 ((𝐺 ∈ USGraph ∧ (𝑥𝑉𝑦𝑉)) → (𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
107, 9sylan 570 . . . . . . . 8 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (𝑥𝑉𝑦𝑉)) → (𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
11102rexbidva 3208 . . . . . . 7 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (∃𝑥𝑉𝑦𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
125, 11syl5bb 273 . . . . . 6 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
1312anbi1d 616 . . . . 5 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁)))
14 19.41vv 2033 . . . . . . 7 (∃𝑥𝑦(((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥𝑦((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁))
15 velsn 4342 . . . . . . . . . . . 12 (𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)
1615bicomi 215 . . . . . . . . . . 11 (𝑧 = ⟨“𝑥𝑁𝑦”⟩ ↔ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})
1716anbi2i 610 . . . . . . . . . 10 ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
1817a1i 11 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
19 simplr 774 . . . . . . . . . . . 12 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) → 𝑁𝑉)
20 anass 455 . . . . . . . . . . . . . . 15 (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ (𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
21 ancom 449 . . . . . . . . . . . . . . 15 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ (𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ↔ ((𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
22 an12 625 . . . . . . . . . . . . . . . . 17 ((𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ (𝑥𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))
23 nesym 3002 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑦 ↔ ¬ 𝑦 = 𝑥)
24 prcom 4414 . . . . . . . . . . . . . . . . . . . 20 {𝑚, 𝑦} = {𝑦, 𝑚}
2524eleq1i 2844 . . . . . . . . . . . . . . . . . . 19 ({𝑚, 𝑦} ∈ (Edg‘𝐺) ↔ {𝑦, 𝑚} ∈ (Edg‘𝐺))
2623, 25anbi12ci 614 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)) ↔ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))
2726anbi2i 610 . . . . . . . . . . . . . . . . 17 (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ (𝑥𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
2822, 27bitri 265 . . . . . . . . . . . . . . . 16 ((𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
2928anbi1i 611 . . . . . . . . . . . . . . 15 (((𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩) ↔ (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
3020, 21, 293bitri 287 . . . . . . . . . . . . . 14 (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
31 preq2 4416 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑁 → {𝑥, 𝑚} = {𝑥, 𝑁})
3231eleq1d 2838 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑁 → ({𝑥, 𝑚} ∈ (Edg‘𝐺) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
33 preq2 4416 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑁 → {𝑦, 𝑚} = {𝑦, 𝑁})
3433eleq1d 2838 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑁 → ({𝑦, 𝑚} ∈ (Edg‘𝐺) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
3534anbi1d 616 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑁 → (({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
3632, 35anbi12d 617 . . . . . . . . . . . . . . 15 (𝑚 = 𝑁 → (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ↔ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))))
37 s3eq2 13846 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑁 → ⟨“𝑥𝑚𝑦”⟩ = ⟨“𝑥𝑁𝑦”⟩)
3837eqeq2d 2784 . . . . . . . . . . . . . . 15 (𝑚 = 𝑁 → (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ↔ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))
3936, 38anbi12d 617 . . . . . . . . . . . . . 14 (𝑚 = 𝑁 → ((({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
4030, 39syl5bb 273 . . . . . . . . . . . . 13 (𝑚 = 𝑁 → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
4140adantl 468 . . . . . . . . . . . 12 ((((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) ∧ 𝑚 = 𝑁) → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
42 fveq1 6347 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → (𝑧‘1) = (⟨“𝑥𝑚𝑦”⟩‘1))
43 vex 3358 . . . . . . . . . . . . . . . . . . . . 21 𝑚 ∈ V
44 s3fv1 13868 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ V → (⟨“𝑥𝑚𝑦”⟩‘1) = 𝑚)
4543, 44ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (⟨“𝑥𝑚𝑦”⟩‘1) = 𝑚
4642, 45syl6eq 2824 . . . . . . . . . . . . . . . . . . 19 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → (𝑧‘1) = 𝑚)
4746eqeq1d 2776 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
4847biimpd 220 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
4948adantr 467 . . . . . . . . . . . . . . . 16 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
5049adantr 467 . . . . . . . . . . . . . . 15 (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
5150com12 32 . . . . . . . . . . . . . 14 ((𝑧‘1) = 𝑁 → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → 𝑚 = 𝑁))
5251ad2antll 709 . . . . . . . . . . . . 13 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → 𝑚 = 𝑁))
5352imp 394 . . . . . . . . . . . 12 ((((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) ∧ ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) → 𝑚 = 𝑁)
5419, 41, 53rspcebdv 3470 . . . . . . . . . . 11 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) → (∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
5554pm5.32da 569 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ↔ (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
56 an32 626 . . . . . . . . . . 11 ((((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
5756a1i 11 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
58 usgrumgr 26317 . . . . . . . . . . . . . . . . . 18 (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph)
591, 8umgrpredgv 26278 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → (𝑥𝑉𝑁𝑉))
6059simpld 483 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → 𝑥𝑉)
6160ex 398 . . . . . . . . . . . . . . . . . . 19 (𝐺 ∈ UMGraph → ({𝑥, 𝑁} ∈ (Edg‘𝐺) → 𝑥𝑉))
621, 8umgrpredgv 26278 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ UMGraph ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → (𝑦𝑉𝑁𝑉))
6362simpld 483 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺 ∈ UMGraph ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → 𝑦𝑉)
6463expcom 399 . . . . . . . . . . . . . . . . . . . . 21 ({𝑦, 𝑁} ∈ (Edg‘𝐺) → (𝐺 ∈ UMGraph → 𝑦𝑉))
6564adantr 467 . . . . . . . . . . . . . . . . . . . 20 (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) → (𝐺 ∈ UMGraph → 𝑦𝑉))
6665com12 32 . . . . . . . . . . . . . . . . . . 19 (𝐺 ∈ UMGraph → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) → 𝑦𝑉))
6761, 66anim12d 597 . . . . . . . . . . . . . . . . . 18 (𝐺 ∈ UMGraph → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥𝑉𝑦𝑉)))
686, 58, 673syl 18 . . . . . . . . . . . . . . . . 17 (𝐺 ∈ FinUSGraph → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥𝑉𝑦𝑉)))
6968adantr 467 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥𝑉𝑦𝑉)))
7069com12 32 . . . . . . . . . . . . . . 15 (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑥𝑉𝑦𝑉)))
7170adantr 467 . . . . . . . . . . . . . 14 ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑥𝑉𝑦𝑉)))
7271impcom 395 . . . . . . . . . . . . 13 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → (𝑥𝑉𝑦𝑉))
73 fveq1 6347 . . . . . . . . . . . . . . 15 (𝑧 = ⟨“𝑥𝑁𝑦”⟩ → (𝑧‘1) = (⟨“𝑥𝑁𝑦”⟩‘1))
7473adantl 468 . . . . . . . . . . . . . 14 ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → (𝑧‘1) = (⟨“𝑥𝑁𝑦”⟩‘1))
75 s3fv1 13868 . . . . . . . . . . . . . . 15 (𝑁𝑉 → (⟨“𝑥𝑁𝑦”⟩‘1) = 𝑁)
7675adantl 468 . . . . . . . . . . . . . 14 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (⟨“𝑥𝑁𝑦”⟩‘1) = 𝑁)
7774, 76sylan9eqr 2830 . . . . . . . . . . . . 13 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → (𝑧‘1) = 𝑁)
7872, 77jca 502 . . . . . . . . . . . 12 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁))
7978ex 398 . . . . . . . . . . 11 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)))
8079pm4.71rd 553 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
8155, 57, 803bitr4d 301 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
828nbusgreledg 26493 . . . . . . . . . . . . 13 (𝐺 ∈ USGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
836, 82syl 17 . . . . . . . . . . . 12 (𝐺 ∈ FinUSGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
8483adantr 467 . . . . . . . . . . 11 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
85 eldif 3739 . . . . . . . . . . . 12 (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}))
868nbusgreledg 26493 . . . . . . . . . . . . . . 15 (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
876, 86syl 17 . . . . . . . . . . . . . 14 (𝐺 ∈ FinUSGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
8887adantr 467 . . . . . . . . . . . . 13 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
89 velsn 4342 . . . . . . . . . . . . . . 15 (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
9089a1i 11 . . . . . . . . . . . . . 14 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥))
9190notbid 308 . . . . . . . . . . . . 13 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (¬ 𝑦 ∈ {𝑥} ↔ ¬ 𝑦 = 𝑥))
9288, 91anbi12d 617 . . . . . . . . . . . 12 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑦 ∈ (𝐺 NeighbVtx 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
9385, 92syl5bb 273 . . . . . . . . . . 11 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
9484, 93anbi12d 617 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ↔ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))))
9594anbi1d 616 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
9618, 81, 953bitr4d 301 . . . . . . . 8 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
97962exbidv 2007 . . . . . . 7 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (∃𝑥𝑦(((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
9814, 97syl5bbr 275 . . . . . 6 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((∃𝑥𝑦((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
99 r2ex 3213 . . . . . . 7 (∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ∃𝑥𝑦((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
10099anbi1i 611 . . . . . 6 ((∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥𝑦((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁))
101 r2ex 3213 . . . . . 6 (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ ∃𝑥𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
10298, 100, 1013bitr4g 304 . . . . 5 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
103 vex 3358 . . . . . . . 8 𝑧 ∈ V
104 eleq1w 2836 . . . . . . . . 9 (𝑝 = 𝑧 → (𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
1051042rexbidv 3209 . . . . . . . 8 (𝑝 = 𝑧 → (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
106103, 105elab 3507 . . . . . . 7 (𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})
107106bicomi 215 . . . . . 6 (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}})
108107a1i 11 . . . . 5 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
10913, 102, 1083bitrd 295 . . . 4 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁) ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
1104, 109bitrd 269 . . 3 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (𝑀𝑁) ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
111110eqrdv 2772 . 2 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑀𝑁) = {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}})
112 dfiunv2 4701 . 2 𝑥 ∈ (𝐺 NeighbVtx 𝑁) 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){⟨“𝑥𝑁𝑦”⟩} = {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}
113111, 112syl6eqr 2826 1 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑀𝑁) = 𝑥 ∈ (𝐺 NeighbVtx 𝑁) 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){⟨“𝑥𝑁𝑦”⟩})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 383   = wceq 1634  wex 1855  wcel 2148  {cab 2760  wne 2946  wrex 3065  {crab 3068  Vcvv 3355  cdif 3726  {csn 4326  {cpr 4328   ciun 4665  cmpt 4876  cfv 6042  (class class class)co 6812  1c1 10160  2c2 11293  ⟨“cs3 13818  Vtxcvtx 26116  Edgcedg 26181  UMGraphcumgr 26218  USGraphcusgr 26287  FinUSGraphcfusgr 26452   NeighbVtx cnbgr 26468   WSPathsN cwwspthsn 26977   WSPathsNOn cwwspthsnon 26978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-rep 4917  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117  ax-ac2 9508  ax-cnex 10215  ax-resscn 10216  ax-1cn 10217  ax-icn 10218  ax-addcl 10219  ax-addrcl 10220  ax-mulcl 10221  ax-mulrcl 10222  ax-mulcom 10223  ax-addass 10224  ax-mulass 10225  ax-distr 10226  ax-i2m1 10227  ax-1ne0 10228  ax-1rid 10229  ax-rnegex 10230  ax-rrecex 10231  ax-cnre 10232  ax-pre-lttri 10233  ax-pre-lttrn 10234  ax-pre-ltadd 10235  ax-pre-mulgt0 10236
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-ifp 1077  df-3or 1099  df-3an 1100  df-tru 1637  df-fal 1640  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-pss 3745  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-tp 4331  df-op 4333  df-uni 4586  df-int 4623  df-iun 4667  df-br 4798  df-opab 4860  df-mpt 4877  df-tr 4900  df-id 5171  df-eprel 5176  df-po 5184  df-so 5185  df-fr 5222  df-se 5223  df-we 5224  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-ord 5880  df-on 5881  df-lim 5882  df-suc 5883  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-isom 6051  df-riota 6773  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-om 7234  df-1st 7336  df-2nd 7337  df-wrecs 7580  df-recs 7642  df-rdg 7680  df-1o 7734  df-2o 7735  df-oadd 7738  df-er 7917  df-map 8032  df-pm 8033  df-en 8131  df-dom 8132  df-sdom 8133  df-fin 8134  df-card 8986  df-ac 9160  df-cda 9213  df-pnf 10299  df-mnf 10300  df-xr 10301  df-ltxr 10302  df-le 10303  df-sub 10491  df-neg 10492  df-nn 11244  df-2 11302  df-3 11303  df-n0 11517  df-xnn0 11588  df-z 11602  df-uz 11911  df-fz 12556  df-fzo 12696  df-hash 13344  df-word 13517  df-concat 13519  df-s1 13520  df-s2 13824  df-s3 13825  df-edg 26182  df-uhgr 26195  df-upgr 26219  df-umgr 26220  df-uspgr 26288  df-usgr 26289  df-fusgr 26453  df-nbgr 26469  df-wlks 26751  df-wlkson 26752  df-trls 26845  df-trlson 26846  df-pths 26868  df-spths 26869  df-pthson 26870  df-spthson 26871  df-wwlks 26979  df-wwlksn 26980  df-wwlksnon 26981  df-wspthsn 26982  df-wspthsnon 26983
This theorem is referenced by:  fusgreghash2wspv  27538
  Copyright terms: Public domain W3C validator