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

Theorem fusgr2wsp2nb 27172
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, 8-Jan-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 27171 . . . . 5 (𝑁𝑉 → (𝑧 ∈ (𝑀𝑁) ↔ (𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁)))
43adantl 482 . . . 4 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (𝑀𝑁) ↔ (𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁)))
5 2nn0 11294 . . . . . . . . 9 2 ∈ ℕ0
61wspthsnwspthsnon 26792 . . . . . . . . 9 ((2 ∈ ℕ0𝐺 ∈ FinUSGraph ) → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥𝑉𝑦𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦)))
75, 6mpan 705 . . . . . . . 8 (𝐺 ∈ FinUSGraph → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥𝑉𝑦𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦)))
87adantr 481 . . . . . . 7 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥𝑉𝑦𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦)))
9 fusgrusgr 26195 . . . . . . . . . 10 (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )
109adantr 481 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → 𝐺 ∈ USGraph )
11 eqid 2620 . . . . . . . . . 10 (Edg‘𝐺) = (Edg‘𝐺)
121, 11usgr2wspthon 26839 . . . . . . . . 9 ((𝐺 ∈ USGraph ∧ (𝑥𝑉𝑦𝑉)) → (𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
1310, 12sylan 488 . . . . . . . 8 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (𝑥𝑉𝑦𝑉)) → (𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
14132rexbidva 3052 . . . . . . 7 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (∃𝑥𝑉𝑦𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
158, 14bitrd 268 . . . . . 6 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
1615anbi1d 740 . . . . 5 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁)))
17 19.41vv 1913 . . . . . . 7 (∃𝑥𝑦(((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥𝑦((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁))
18 velsn 4184 . . . . . . . . . . . 12 (𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)
1918bicomi 214 . . . . . . . . . . 11 (𝑧 = ⟨“𝑥𝑁𝑦”⟩ ↔ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})
2019anbi2i 729 . . . . . . . . . 10 ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
2120a1i 11 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
22 simplr 791 . . . . . . . . . . . 12 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) → 𝑁𝑉)
23 anass 680 . . . . . . . . . . . . . . 15 (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ (𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
24 ancom 466 . . . . . . . . . . . . . . 15 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ (𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ↔ ((𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
25 an12 837 . . . . . . . . . . . . . . . . 17 ((𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ (𝑥𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))
26 nesym 2847 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑦 ↔ ¬ 𝑦 = 𝑥)
27 prcom 4258 . . . . . . . . . . . . . . . . . . . 20 {𝑚, 𝑦} = {𝑦, 𝑚}
2827eleq1i 2690 . . . . . . . . . . . . . . . . . . 19 ({𝑚, 𝑦} ∈ (Edg‘𝐺) ↔ {𝑦, 𝑚} ∈ (Edg‘𝐺))
2926, 28anbi12ci 733 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)) ↔ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))
3029anbi2i 729 . . . . . . . . . . . . . . . . 17 (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ (𝑥𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
3125, 30bitri 264 . . . . . . . . . . . . . . . 16 ((𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
3231anbi1i 730 . . . . . . . . . . . . . . 15 (((𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩) ↔ (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
3323, 24, 323bitri 286 . . . . . . . . . . . . . 14 (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
34 preq2 4260 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑁 → {𝑥, 𝑚} = {𝑥, 𝑁})
3534eleq1d 2684 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑁 → ({𝑥, 𝑚} ∈ (Edg‘𝐺) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
36 preq2 4260 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑁 → {𝑦, 𝑚} = {𝑦, 𝑁})
3736eleq1d 2684 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑁 → ({𝑦, 𝑚} ∈ (Edg‘𝐺) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
3837anbi1d 740 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑁 → (({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
3935, 38anbi12d 746 . . . . . . . . . . . . . . 15 (𝑚 = 𝑁 → (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ↔ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))))
40 s3eq2 13596 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑁 → ⟨“𝑥𝑚𝑦”⟩ = ⟨“𝑥𝑁𝑦”⟩)
4140eqeq2d 2630 . . . . . . . . . . . . . . 15 (𝑚 = 𝑁 → (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ↔ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))
4239, 41anbi12d 746 . . . . . . . . . . . . . 14 (𝑚 = 𝑁 → ((({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
4333, 42syl5bb 272 . . . . . . . . . . . . 13 (𝑚 = 𝑁 → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
4443adantl 482 . . . . . . . . . . . 12 ((((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) ∧ 𝑚 = 𝑁) → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
45 fveq1 6177 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → (𝑧‘1) = (⟨“𝑥𝑚𝑦”⟩‘1))
46 vex 3198 . . . . . . . . . . . . . . . . . . . . 21 𝑚 ∈ V
47 s3fv1 13618 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ V → (⟨“𝑥𝑚𝑦”⟩‘1) = 𝑚)
4846, 47ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (⟨“𝑥𝑚𝑦”⟩‘1) = 𝑚
4945, 48syl6eq 2670 . . . . . . . . . . . . . . . . . . 19 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → (𝑧‘1) = 𝑚)
5049eqeq1d 2622 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
5150biimpd 219 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
5251adantr 481 . . . . . . . . . . . . . . . 16 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
5352adantr 481 . . . . . . . . . . . . . . 15 (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
5453com12 32 . . . . . . . . . . . . . 14 ((𝑧‘1) = 𝑁 → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → 𝑚 = 𝑁))
5554ad2antll 764 . . . . . . . . . . . . 13 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → 𝑚 = 𝑁))
5655imp 445 . . . . . . . . . . . 12 ((((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) ∧ ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) → 𝑚 = 𝑁)
5722, 44, 56rspcebdv 3309 . . . . . . . . . . 11 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) → (∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
5857pm5.32da 672 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ↔ (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
59 an32 838 . . . . . . . . . . 11 ((((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
6059a1i 11 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
61 usgrumgr 26055 . . . . . . . . . . . . . . . . . 18 (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
621, 11umgrpredgv 26016 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → (𝑥𝑉𝑁𝑉))
6362simpld 475 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → 𝑥𝑉)
6463ex 450 . . . . . . . . . . . . . . . . . . 19 (𝐺 ∈ UMGraph → ({𝑥, 𝑁} ∈ (Edg‘𝐺) → 𝑥𝑉))
651, 11umgrpredgv 26016 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ UMGraph ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → (𝑦𝑉𝑁𝑉))
6665simpld 475 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺 ∈ UMGraph ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → 𝑦𝑉)
6766expcom 451 . . . . . . . . . . . . . . . . . . . . 21 ({𝑦, 𝑁} ∈ (Edg‘𝐺) → (𝐺 ∈ UMGraph → 𝑦𝑉))
6867adantr 481 . . . . . . . . . . . . . . . . . . . 20 (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) → (𝐺 ∈ UMGraph → 𝑦𝑉))
6968com12 32 . . . . . . . . . . . . . . . . . . 19 (𝐺 ∈ UMGraph → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) → 𝑦𝑉))
7064, 69anim12d 585 . . . . . . . . . . . . . . . . . 18 (𝐺 ∈ UMGraph → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥𝑉𝑦𝑉)))
719, 61, 703syl 18 . . . . . . . . . . . . . . . . 17 (𝐺 ∈ FinUSGraph → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥𝑉𝑦𝑉)))
7271adantr 481 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥𝑉𝑦𝑉)))
7372com12 32 . . . . . . . . . . . . . . 15 (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑥𝑉𝑦𝑉)))
7473adantr 481 . . . . . . . . . . . . . 14 ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑥𝑉𝑦𝑉)))
7574impcom 446 . . . . . . . . . . . . 13 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → (𝑥𝑉𝑦𝑉))
76 fveq1 6177 . . . . . . . . . . . . . . 15 (𝑧 = ⟨“𝑥𝑁𝑦”⟩ → (𝑧‘1) = (⟨“𝑥𝑁𝑦”⟩‘1))
7776adantl 482 . . . . . . . . . . . . . 14 ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → (𝑧‘1) = (⟨“𝑥𝑁𝑦”⟩‘1))
78 s3fv1 13618 . . . . . . . . . . . . . . 15 (𝑁𝑉 → (⟨“𝑥𝑁𝑦”⟩‘1) = 𝑁)
7978adantl 482 . . . . . . . . . . . . . 14 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (⟨“𝑥𝑁𝑦”⟩‘1) = 𝑁)
8077, 79sylan9eqr 2676 . . . . . . . . . . . . 13 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → (𝑧‘1) = 𝑁)
8175, 80jca 554 . . . . . . . . . . . 12 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁))
8281ex 450 . . . . . . . . . . 11 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)))
8382pm4.71rd 666 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
8458, 60, 833bitr4d 300 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
8511nbusgreledg 26230 . . . . . . . . . . . . 13 (𝐺 ∈ USGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
869, 85syl 17 . . . . . . . . . . . 12 (𝐺 ∈ FinUSGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
8786adantr 481 . . . . . . . . . . 11 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
88 eldif 3577 . . . . . . . . . . . 12 (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}))
8911nbusgreledg 26230 . . . . . . . . . . . . . . 15 (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
909, 89syl 17 . . . . . . . . . . . . . 14 (𝐺 ∈ FinUSGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
9190adantr 481 . . . . . . . . . . . . 13 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
92 velsn 4184 . . . . . . . . . . . . . . 15 (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
9392a1i 11 . . . . . . . . . . . . . 14 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥))
9493notbid 308 . . . . . . . . . . . . 13 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (¬ 𝑦 ∈ {𝑥} ↔ ¬ 𝑦 = 𝑥))
9591, 94anbi12d 746 . . . . . . . . . . . 12 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑦 ∈ (𝐺 NeighbVtx 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
9688, 95syl5bb 272 . . . . . . . . . . 11 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
9787, 96anbi12d 746 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ↔ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))))
9897anbi1d 740 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
9921, 84, 983bitr4d 300 . . . . . . . 8 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
100992exbidv 1850 . . . . . . 7 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (∃𝑥𝑦(((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
10117, 100syl5bbr 274 . . . . . 6 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((∃𝑥𝑦((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
102 r2ex 3057 . . . . . . 7 (∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ∃𝑥𝑦((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
103102anbi1i 730 . . . . . 6 ((∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥𝑦((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁))
104 r2ex 3057 . . . . . 6 (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ ∃𝑥𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
105101, 103, 1043bitr4g 303 . . . . 5 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
106 vex 3198 . . . . . . . 8 𝑧 ∈ V
107 eleq1w 2682 . . . . . . . . 9 (𝑝 = 𝑧 → (𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
1081072rexbidv 3053 . . . . . . . 8 (𝑝 = 𝑧 → (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
109106, 108elab 3344 . . . . . . 7 (𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})
110109bicomi 214 . . . . . 6 (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}})
111110a1i 11 . . . . 5 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
11216, 105, 1113bitrd 294 . . . 4 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁) ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
1134, 112bitrd 268 . . 3 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (𝑀𝑁) ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
114113eqrdv 2618 . 2 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑀𝑁) = {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}})
115 dfiunv2 4547 . 2 𝑥 ∈ (𝐺 NeighbVtx 𝑁) 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){⟨“𝑥𝑁𝑦”⟩} = {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}
116114, 115syl6eqr 2672 1 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑀𝑁) = 𝑥 ∈ (𝐺 NeighbVtx 𝑁) 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){⟨“𝑥𝑁𝑦”⟩})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1481  wex 1702  wcel 1988  {cab 2606  wne 2791  wrex 2910  {crab 2913  Vcvv 3195  cdif 3564  {csn 4168  {cpr 4170   ciun 4511  cmpt 4720  cfv 5876  (class class class)co 6635  1c1 9922  2c2 11055  0cn0 11277  ⟨“cs3 13568  Vtxcvtx 25855  Edgcedg 25920   UMGraph cumgr 25957   USGraph cusgr 26025   FinUSGraph cfusgr 26189   NeighbVtx cnbgr 26205   WSPathsN cwwspthsn 26701   WSPathsNOn cwwspthsnon 26702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-ac2 9270  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ifp 1012  df-3or 1037  df-3an 1038  df-tru 1484  df-fal 1487  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-2o 7546  df-oadd 7549  df-er 7727  df-map 7844  df-pm 7845  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-card 8750  df-ac 8924  df-cda 8975  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-nn 11006  df-2 11064  df-3 11065  df-n0 11278  df-xnn0 11349  df-z 11363  df-uz 11673  df-fz 12312  df-fzo 12450  df-hash 13101  df-word 13282  df-concat 13284  df-s1 13285  df-s2 13574  df-s3 13575  df-edg 25921  df-uhgr 25934  df-upgr 25958  df-umgr 25959  df-uspgr 26026  df-usgr 26027  df-fusgr 26190  df-nbgr 26209  df-wlks 26476  df-wlkson 26477  df-trls 26570  df-trlson 26571  df-pths 26593  df-spths 26594  df-pthson 26595  df-spthson 26596  df-wwlks 26703  df-wwlksn 26704  df-wwlksnon 26705  df-wspthsn 26706  df-wspthsnon 26707
This theorem is referenced by:  fusgreghash2wspv  27173
  Copyright terms: Public domain W3C validator