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

Theorem fusgr2wsp2nb 28105
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 28104 . . . . 5 (𝑁𝑉 → (𝑧 ∈ (𝑀𝑁) ↔ (𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁)))
43adantl 484 . . . 4 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (𝑀𝑁) ↔ (𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁)))
51wspthsnwspthsnon 27687 . . . . . . 7 (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥𝑉𝑦𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦))
6 fusgrusgr 27096 . . . . . . . . . 10 (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph)
76adantr 483 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → 𝐺 ∈ USGraph)
8 eqid 2819 . . . . . . . . . 10 (Edg‘𝐺) = (Edg‘𝐺)
91, 8usgr2wspthon 27736 . . . . . . . . 9 ((𝐺 ∈ USGraph ∧ (𝑥𝑉𝑦𝑉)) → (𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
107, 9sylan 582 . . . . . . . 8 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (𝑥𝑉𝑦𝑉)) → (𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
11102rexbidva 3297 . . . . . . 7 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (∃𝑥𝑉𝑦𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
125, 11syl5bb 285 . . . . . 6 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
1312anbi1d 631 . . . . 5 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁)))
14 19.41vv 1944 . . . . . . 7 (∃𝑥𝑦(((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥𝑦((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁))
15 velsn 4575 . . . . . . . . . . . 12 (𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)
1615bicomi 226 . . . . . . . . . . 11 (𝑧 = ⟨“𝑥𝑁𝑦”⟩ ↔ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})
1716anbi2i 624 . . . . . . . . . 10 ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
1817a1i 11 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
19 simplr 767 . . . . . . . . . . . 12 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) → 𝑁𝑉)
20 anass 471 . . . . . . . . . . . . . . 15 (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ (𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
21 ancom 463 . . . . . . . . . . . . . . 15 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ (𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ↔ ((𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
22 an12 643 . . . . . . . . . . . . . . . . 17 ((𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ (𝑥𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))
23 nesym 3070 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑦 ↔ ¬ 𝑦 = 𝑥)
24 prcom 4660 . . . . . . . . . . . . . . . . . . . 20 {𝑚, 𝑦} = {𝑦, 𝑚}
2524eleq1i 2901 . . . . . . . . . . . . . . . . . . 19 ({𝑚, 𝑦} ∈ (Edg‘𝐺) ↔ {𝑦, 𝑚} ∈ (Edg‘𝐺))
2623, 25anbi12ci 629 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)) ↔ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))
2726anbi2i 624 . . . . . . . . . . . . . . . . 17 (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ (𝑥𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
2822, 27bitri 277 . . . . . . . . . . . . . . . 16 ((𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
2928anbi1i 625 . . . . . . . . . . . . . . 15 (((𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩) ↔ (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
3020, 21, 293bitri 299 . . . . . . . . . . . . . 14 (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
31 preq2 4662 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑁 → {𝑥, 𝑚} = {𝑥, 𝑁})
3231eleq1d 2895 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑁 → ({𝑥, 𝑚} ∈ (Edg‘𝐺) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
33 preq2 4662 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑁 → {𝑦, 𝑚} = {𝑦, 𝑁})
3433eleq1d 2895 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑁 → ({𝑦, 𝑚} ∈ (Edg‘𝐺) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
3534anbi1d 631 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑁 → (({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
3632, 35anbi12d 632 . . . . . . . . . . . . . . 15 (𝑚 = 𝑁 → (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ↔ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))))
37 s3eq2 14224 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑁 → ⟨“𝑥𝑚𝑦”⟩ = ⟨“𝑥𝑁𝑦”⟩)
3837eqeq2d 2830 . . . . . . . . . . . . . . 15 (𝑚 = 𝑁 → (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ↔ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))
3936, 38anbi12d 632 . . . . . . . . . . . . . 14 (𝑚 = 𝑁 → ((({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
4030, 39syl5bb 285 . . . . . . . . . . . . 13 (𝑚 = 𝑁 → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
4140adantl 484 . . . . . . . . . . . 12 ((((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) ∧ 𝑚 = 𝑁) → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
42 fveq1 6662 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → (𝑧‘1) = (⟨“𝑥𝑚𝑦”⟩‘1))
43 s3fv1 14246 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ V → (⟨“𝑥𝑚𝑦”⟩‘1) = 𝑚)
4443elv 3498 . . . . . . . . . . . . . . . . . . . 20 (⟨“𝑥𝑚𝑦”⟩‘1) = 𝑚
4542, 44syl6eq 2870 . . . . . . . . . . . . . . . . . . 19 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → (𝑧‘1) = 𝑚)
4645eqeq1d 2821 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
4746biimpd 231 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
4847adantr 483 . . . . . . . . . . . . . . . 16 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
4948adantr 483 . . . . . . . . . . . . . . 15 (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
5049com12 32 . . . . . . . . . . . . . 14 ((𝑧‘1) = 𝑁 → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → 𝑚 = 𝑁))
5150ad2antll 727 . . . . . . . . . . . . 13 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → 𝑚 = 𝑁))
5251imp 409 . . . . . . . . . . . 12 ((((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) ∧ ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) → 𝑚 = 𝑁)
5319, 41, 52rspcebdv 3615 . . . . . . . . . . 11 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) → (∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
5453pm5.32da 581 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ↔ (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
55 an32 644 . . . . . . . . . . 11 ((((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
5655a1i 11 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
57 usgrumgr 26956 . . . . . . . . . . . . . . . . . 18 (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph)
581, 8umgrpredgv 26917 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → (𝑥𝑉𝑁𝑉))
5958simpld 497 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → 𝑥𝑉)
6059ex 415 . . . . . . . . . . . . . . . . . . 19 (𝐺 ∈ UMGraph → ({𝑥, 𝑁} ∈ (Edg‘𝐺) → 𝑥𝑉))
611, 8umgrpredgv 26917 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ UMGraph ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → (𝑦𝑉𝑁𝑉))
6261simpld 497 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺 ∈ UMGraph ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → 𝑦𝑉)
6362expcom 416 . . . . . . . . . . . . . . . . . . . . 21 ({𝑦, 𝑁} ∈ (Edg‘𝐺) → (𝐺 ∈ UMGraph → 𝑦𝑉))
6463adantr 483 . . . . . . . . . . . . . . . . . . . 20 (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) → (𝐺 ∈ UMGraph → 𝑦𝑉))
6564com12 32 . . . . . . . . . . . . . . . . . . 19 (𝐺 ∈ UMGraph → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) → 𝑦𝑉))
6660, 65anim12d 610 . . . . . . . . . . . . . . . . . 18 (𝐺 ∈ UMGraph → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥𝑉𝑦𝑉)))
676, 57, 663syl 18 . . . . . . . . . . . . . . . . 17 (𝐺 ∈ FinUSGraph → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥𝑉𝑦𝑉)))
6867adantr 483 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥𝑉𝑦𝑉)))
6968com12 32 . . . . . . . . . . . . . . 15 (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑥𝑉𝑦𝑉)))
7069adantr 483 . . . . . . . . . . . . . 14 ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑥𝑉𝑦𝑉)))
7170impcom 410 . . . . . . . . . . . . 13 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → (𝑥𝑉𝑦𝑉))
72 fveq1 6662 . . . . . . . . . . . . . . 15 (𝑧 = ⟨“𝑥𝑁𝑦”⟩ → (𝑧‘1) = (⟨“𝑥𝑁𝑦”⟩‘1))
7372adantl 484 . . . . . . . . . . . . . 14 ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → (𝑧‘1) = (⟨“𝑥𝑁𝑦”⟩‘1))
74 s3fv1 14246 . . . . . . . . . . . . . . 15 (𝑁𝑉 → (⟨“𝑥𝑁𝑦”⟩‘1) = 𝑁)
7574adantl 484 . . . . . . . . . . . . . 14 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (⟨“𝑥𝑁𝑦”⟩‘1) = 𝑁)
7673, 75sylan9eqr 2876 . . . . . . . . . . . . 13 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → (𝑧‘1) = 𝑁)
7771, 76jca 514 . . . . . . . . . . . 12 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁))
7877ex 415 . . . . . . . . . . 11 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)))
7978pm4.71rd 565 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
8054, 56, 793bitr4d 313 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
818nbusgreledg 27127 . . . . . . . . . . . . 13 (𝐺 ∈ USGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
826, 81syl 17 . . . . . . . . . . . 12 (𝐺 ∈ FinUSGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
8382adantr 483 . . . . . . . . . . 11 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
84 eldif 3944 . . . . . . . . . . . 12 (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}))
858nbusgreledg 27127 . . . . . . . . . . . . . . 15 (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
866, 85syl 17 . . . . . . . . . . . . . 14 (𝐺 ∈ FinUSGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
8786adantr 483 . . . . . . . . . . . . 13 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
88 velsn 4575 . . . . . . . . . . . . . . 15 (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
8988a1i 11 . . . . . . . . . . . . . 14 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥))
9089notbid 320 . . . . . . . . . . . . 13 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (¬ 𝑦 ∈ {𝑥} ↔ ¬ 𝑦 = 𝑥))
9187, 90anbi12d 632 . . . . . . . . . . . 12 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑦 ∈ (𝐺 NeighbVtx 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
9284, 91syl5bb 285 . . . . . . . . . . 11 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
9383, 92anbi12d 632 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ↔ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))))
9493anbi1d 631 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
9518, 80, 943bitr4d 313 . . . . . . . 8 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
96952exbidv 1918 . . . . . . 7 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (∃𝑥𝑦(((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
9714, 96syl5bbr 287 . . . . . 6 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((∃𝑥𝑦((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
98 r2ex 3301 . . . . . . 7 (∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ∃𝑥𝑦((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
9998anbi1i 625 . . . . . 6 ((∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥𝑦((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁))
100 r2ex 3301 . . . . . 6 (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ ∃𝑥𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
10197, 99, 1003bitr4g 316 . . . . 5 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
102 vex 3496 . . . . . . . 8 𝑧 ∈ V
103 eleq1w 2893 . . . . . . . . 9 (𝑝 = 𝑧 → (𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
1041032rexbidv 3298 . . . . . . . 8 (𝑝 = 𝑧 → (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
105102, 104elab 3665 . . . . . . 7 (𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})
106105bicomi 226 . . . . . 6 (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}})
107106a1i 11 . . . . 5 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
10813, 101, 1073bitrd 307 . . . 4 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁) ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
1094, 108bitrd 281 . . 3 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (𝑀𝑁) ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
110109eqrdv 2817 . 2 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑀𝑁) = {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}})
111 dfiunv2 4951 . 2 𝑥 ∈ (𝐺 NeighbVtx 𝑁) 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){⟨“𝑥𝑁𝑦”⟩} = {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}
112110, 111syl6eqr 2872 1 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑀𝑁) = 𝑥 ∈ (𝐺 NeighbVtx 𝑁) 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){⟨“𝑥𝑁𝑦”⟩})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398   = wceq 1530  wex 1773  wcel 2107  {cab 2797  wne 3014  wrex 3137  {crab 3140  Vcvv 3493  cdif 3931  {csn 4559  {cpr 4561   ciun 4910  cmpt 5137  cfv 6348  (class class class)co 7148  1c1 10530  2c2 11684  ⟨“cs3 14196  Vtxcvtx 26773  Edgcedg 26824  UMGraphcumgr 26858  USGraphcusgr 26926  FinUSGraphcfusgr 27090   NeighbVtx cnbgr 27106   WSPathsN cwwspthsn 27598   WSPathsNOn cwwspthsnon 27599
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-ac2 9877  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ifp 1057  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-2o 8095  df-oadd 8098  df-er 8281  df-map 8400  df-pm 8401  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-dju 9322  df-card 9360  df-ac 9534  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-2 11692  df-3 11693  df-n0 11890  df-xnn0 11960  df-z 11974  df-uz 12236  df-fz 12885  df-fzo 13026  df-hash 13683  df-word 13854  df-concat 13915  df-s1 13942  df-s2 14202  df-s3 14203  df-edg 26825  df-uhgr 26835  df-upgr 26859  df-umgr 26860  df-uspgr 26927  df-usgr 26928  df-fusgr 27091  df-nbgr 27107  df-wlks 27373  df-wlkson 27374  df-trls 27466  df-trlson 27467  df-pths 27489  df-spths 27490  df-pthson 27491  df-spthson 27492  df-wwlks 27600  df-wwlksn 27601  df-wwlksnon 27602  df-wspthsn 27603  df-wspthsnon 27604
This theorem is referenced by:  fusgreghash2wspv  28106
  Copyright terms: Public domain W3C validator