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

Theorem fusgr2wsp2nb 30353
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 30352 . . . . 5 (𝑁𝑉 → (𝑧 ∈ (𝑀𝑁) ↔ (𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁)))
43adantl 481 . . . 4 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (𝑀𝑁) ↔ (𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁)))
51wspthsnwspthsnon 29936 . . . . . . 7 (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥𝑉𝑦𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦))
6 fusgrusgr 29339 . . . . . . . . . 10 (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph)
76adantr 480 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → 𝐺 ∈ USGraph)
8 eqid 2737 . . . . . . . . . 10 (Edg‘𝐺) = (Edg‘𝐺)
91, 8usgr2wspthon 29985 . . . . . . . . 9 ((𝐺 ∈ USGraph ∧ (𝑥𝑉𝑦𝑉)) → (𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
107, 9sylan 580 . . . . . . . 8 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (𝑥𝑉𝑦𝑉)) → (𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
11102rexbidva 3220 . . . . . . 7 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (∃𝑥𝑉𝑦𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
125, 11bitrid 283 . . . . . 6 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
1312anbi1d 631 . . . . 5 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁)))
14 19.41vv 1950 . . . . . . 7 (∃𝑥𝑦(((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥𝑦((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁))
15 velsn 4642 . . . . . . . . . . . 12 (𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)
1615bicomi 224 . . . . . . . . . . 11 (𝑧 = ⟨“𝑥𝑁𝑦”⟩ ↔ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})
1716anbi2i 623 . . . . . . . . . 10 ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
1817a1i 11 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
19 simplr 769 . . . . . . . . . . . 12 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) → 𝑁𝑉)
20 anass 468 . . . . . . . . . . . . . . 15 (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ (𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
21 ancom 460 . . . . . . . . . . . . . . 15 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ (𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ↔ ((𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
22 an12 645 . . . . . . . . . . . . . . . . 17 ((𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ (𝑥𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))
23 nesym 2997 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑦 ↔ ¬ 𝑦 = 𝑥)
24 prcom 4732 . . . . . . . . . . . . . . . . . . . 20 {𝑚, 𝑦} = {𝑦, 𝑚}
2524eleq1i 2832 . . . . . . . . . . . . . . . . . . 19 ({𝑚, 𝑦} ∈ (Edg‘𝐺) ↔ {𝑦, 𝑚} ∈ (Edg‘𝐺))
2623, 25anbi12ci 629 . . . . . . . . . . . . . . . . . 18 ((𝑥𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)) ↔ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))
2726anbi2i 623 . . . . . . . . . . . . . . . . 17 (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ (𝑥𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
2822, 27bitri 275 . . . . . . . . . . . . . . . 16 ((𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
2928anbi1i 624 . . . . . . . . . . . . . . 15 (((𝑥𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩) ↔ (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
3020, 21, 293bitri 297 . . . . . . . . . . . . . 14 (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
31 preq2 4734 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑁 → {𝑥, 𝑚} = {𝑥, 𝑁})
3231eleq1d 2826 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑁 → ({𝑥, 𝑚} ∈ (Edg‘𝐺) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
33 preq2 4734 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑁 → {𝑦, 𝑚} = {𝑦, 𝑁})
3433eleq1d 2826 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑁 → ({𝑦, 𝑚} ∈ (Edg‘𝐺) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
3534anbi1d 631 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑁 → (({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
3632, 35anbi12d 632 . . . . . . . . . . . . . . 15 (𝑚 = 𝑁 → (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ↔ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))))
37 s3eq2 14909 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑁 → ⟨“𝑥𝑚𝑦”⟩ = ⟨“𝑥𝑁𝑦”⟩)
3837eqeq2d 2748 . . . . . . . . . . . . . . 15 (𝑚 = 𝑁 → (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ↔ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))
3936, 38anbi12d 632 . . . . . . . . . . . . . 14 (𝑚 = 𝑁 → ((({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
4030, 39bitrid 283 . . . . . . . . . . . . 13 (𝑚 = 𝑁 → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
4140adantl 481 . . . . . . . . . . . 12 ((((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) ∧ 𝑚 = 𝑁) → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
42 fveq1 6905 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → (𝑧‘1) = (⟨“𝑥𝑚𝑦”⟩‘1))
43 s3fv1 14931 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ V → (⟨“𝑥𝑚𝑦”⟩‘1) = 𝑚)
4443elv 3485 . . . . . . . . . . . . . . . . . . . 20 (⟨“𝑥𝑚𝑦”⟩‘1) = 𝑚
4542, 44eqtrdi 2793 . . . . . . . . . . . . . . . . . . 19 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → (𝑧‘1) = 𝑚)
4645eqeq1d 2739 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
4746biimpd 229 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
4847adantr 480 . . . . . . . . . . . . . . . 16 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
4948adantr 480 . . . . . . . . . . . . . . 15 (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
5049com12 32 . . . . . . . . . . . . . 14 ((𝑧‘1) = 𝑁 → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → 𝑚 = 𝑁))
5150ad2antll 729 . . . . . . . . . . . . 13 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → 𝑚 = 𝑁))
5251imp 406 . . . . . . . . . . . 12 ((((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) ∧ ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) → 𝑚 = 𝑁)
5319, 41, 52rspcebdv 3616 . . . . . . . . . . 11 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)) → (∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
5453pm5.32da 579 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ↔ (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
55 an32 646 . . . . . . . . . . 11 ((((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
5655a1i 11 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
57 usgrumgr 29198 . . . . . . . . . . . . . . . . . 18 (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph)
581, 8umgrpredgv 29157 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → (𝑥𝑉𝑁𝑉))
5958simpld 494 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → 𝑥𝑉)
6059ex 412 . . . . . . . . . . . . . . . . . . 19 (𝐺 ∈ UMGraph → ({𝑥, 𝑁} ∈ (Edg‘𝐺) → 𝑥𝑉))
611, 8umgrpredgv 29157 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ UMGraph ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → (𝑦𝑉𝑁𝑉))
6261simpld 494 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺 ∈ UMGraph ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → 𝑦𝑉)
6362expcom 413 . . . . . . . . . . . . . . . . . . . . 21 ({𝑦, 𝑁} ∈ (Edg‘𝐺) → (𝐺 ∈ UMGraph → 𝑦𝑉))
6463adantr 480 . . . . . . . . . . . . . . . . . . . 20 (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) → (𝐺 ∈ UMGraph → 𝑦𝑉))
6564com12 32 . . . . . . . . . . . . . . . . . . 19 (𝐺 ∈ UMGraph → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) → 𝑦𝑉))
6660, 65anim12d 609 . . . . . . . . . . . . . . . . . 18 (𝐺 ∈ UMGraph → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥𝑉𝑦𝑉)))
676, 57, 663syl 18 . . . . . . . . . . . . . . . . 17 (𝐺 ∈ FinUSGraph → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥𝑉𝑦𝑉)))
6867adantr 480 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥𝑉𝑦𝑉)))
6968com12 32 . . . . . . . . . . . . . . 15 (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑥𝑉𝑦𝑉)))
7069adantr 480 . . . . . . . . . . . . . 14 ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑥𝑉𝑦𝑉)))
7170impcom 407 . . . . . . . . . . . . 13 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → (𝑥𝑉𝑦𝑉))
72 fveq1 6905 . . . . . . . . . . . . . . 15 (𝑧 = ⟨“𝑥𝑁𝑦”⟩ → (𝑧‘1) = (⟨“𝑥𝑁𝑦”⟩‘1))
7372adantl 481 . . . . . . . . . . . . . 14 ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → (𝑧‘1) = (⟨“𝑥𝑁𝑦”⟩‘1))
74 s3fv1 14931 . . . . . . . . . . . . . . 15 (𝑁𝑉 → (⟨“𝑥𝑁𝑦”⟩‘1) = 𝑁)
7574adantl 481 . . . . . . . . . . . . . 14 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (⟨“𝑥𝑁𝑦”⟩‘1) = 𝑁)
7673, 75sylan9eqr 2799 . . . . . . . . . . . . 13 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → (𝑧‘1) = 𝑁)
7771, 76jca 511 . . . . . . . . . . . 12 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁))
7877ex 412 . . . . . . . . . . 11 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → ((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁)))
7978pm4.71rd 562 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
8054, 56, 793bitr4d 311 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
818nbusgreledg 29370 . . . . . . . . . . . . 13 (𝐺 ∈ USGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
826, 81syl 17 . . . . . . . . . . . 12 (𝐺 ∈ FinUSGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
8382adantr 480 . . . . . . . . . . 11 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
84 eldif 3961 . . . . . . . . . . . 12 (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}))
858nbusgreledg 29370 . . . . . . . . . . . . . . 15 (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
866, 85syl 17 . . . . . . . . . . . . . 14 (𝐺 ∈ FinUSGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
8786adantr 480 . . . . . . . . . . . . 13 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
88 velsn 4642 . . . . . . . . . . . . . . 15 (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
8988a1i 11 . . . . . . . . . . . . . 14 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥))
9089notbid 318 . . . . . . . . . . . . 13 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (¬ 𝑦 ∈ {𝑥} ↔ ¬ 𝑦 = 𝑥))
9187, 90anbi12d 632 . . . . . . . . . . . 12 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑦 ∈ (𝐺 NeighbVtx 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
9284, 91bitrid 283 . . . . . . . . . . 11 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
9383, 92anbi12d 632 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ↔ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))))
9493anbi1d 631 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
9518, 80, 943bitr4d 311 . . . . . . . 8 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
96952exbidv 1924 . . . . . . 7 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (∃𝑥𝑦(((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
9714, 96bitr3id 285 . . . . . 6 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((∃𝑥𝑦((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
98 r2ex 3196 . . . . . . 7 (∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ∃𝑥𝑦((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
9998anbi1i 624 . . . . . 6 ((∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥𝑦((𝑥𝑉𝑦𝑉) ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁))
100 r2ex 3196 . . . . . 6 (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ ∃𝑥𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
10197, 99, 1003bitr4g 314 . . . . 5 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
102 vex 3484 . . . . . . . 8 𝑧 ∈ V
103 eleq1w 2824 . . . . . . . . 9 (𝑝 = 𝑧 → (𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
1041032rexbidv 3222 . . . . . . . 8 (𝑝 = 𝑧 → (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
105102, 104elab 3679 . . . . . . 7 (𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})
106105bicomi 224 . . . . . 6 (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}})
107106a1i 11 . . . . 5 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
10813, 101, 1073bitrd 305 . . . 4 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁) ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
1094, 108bitrd 279 . . 3 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (𝑀𝑁) ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
110109eqrdv 2735 . 2 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑀𝑁) = {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}})
111 dfiunv2 5035 . 2 𝑥 ∈ (𝐺 NeighbVtx 𝑁) 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){⟨“𝑥𝑁𝑦”⟩} = {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}
112110, 111eqtr4di 2795 1 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑀𝑁) = 𝑥 ∈ (𝐺 NeighbVtx 𝑁) 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){⟨“𝑥𝑁𝑦”⟩})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1540  wex 1779  wcel 2108  {cab 2714  wne 2940  wrex 3070  {crab 3436  Vcvv 3480  cdif 3948  {csn 4626  {cpr 4628   ciun 4991  cmpt 5225  cfv 6561  (class class class)co 7431  1c1 11156  2c2 12321  ⟨“cs3 14881  Vtxcvtx 29013  Edgcedg 29064  UMGraphcumgr 29098  USGraphcusgr 29166  FinUSGraphcfusgr 29333   NeighbVtx cnbgr 29349   WSPathsN cwwspthsn 29848   WSPathsNOn cwwspthsnon 29849
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-ac2 10503  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ifp 1064  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-map 8868  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-dju 9941  df-card 9979  df-ac 10156  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-xnn0 12600  df-z 12614  df-uz 12879  df-fz 13548  df-fzo 13695  df-hash 14370  df-word 14553  df-concat 14609  df-s1 14634  df-s2 14887  df-s3 14888  df-edg 29065  df-uhgr 29075  df-upgr 29099  df-umgr 29100  df-uspgr 29167  df-usgr 29168  df-fusgr 29334  df-nbgr 29350  df-wlks 29617  df-wlkson 29618  df-trls 29710  df-trlson 29711  df-pths 29734  df-spths 29735  df-pthson 29736  df-spthson 29737  df-wwlks 29850  df-wwlksn 29851  df-wwlksnon 29852  df-wspthsn 29853  df-wspthsnon 29854
This theorem is referenced by:  fusgreghash2wspv  30354
  Copyright terms: Public domain W3C validator