Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fusgr2wsp2nb Structured version   Visualization version   GIF version

Theorem fusgr2wsp2nb 41496
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.)
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 simpr 475 . . . . 5 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → 𝑁𝑉)
2 ovex 6551 . . . . . 6 (2 WSPathsN 𝐺) ∈ V
32rabex 4731 . . . . 5 {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁} ∈ V
4 eqeq2 2616 . . . . . . . 8 (𝑎 = 𝑁 → ((𝑤‘1) = 𝑎 ↔ (𝑤‘1) = 𝑁))
54rabbidv 3159 . . . . . . 7 (𝑎 = 𝑁 → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎} = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁})
6 fusgreg2wsp.m . . . . . . 7 𝑀 = (𝑎𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})
75, 6fvmptg 6170 . . . . . 6 ((𝑁𝑉 ∧ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁} ∈ V) → (𝑀𝑁) = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁})
87eleq2d 2668 . . . . 5 ((𝑁𝑉 ∧ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁} ∈ V) → (𝑧 ∈ (𝑀𝑁) ↔ 𝑧 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁}))
91, 3, 8sylancl 692 . . . 4 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (𝑀𝑁) ↔ 𝑧 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁}))
10 fveq1 6083 . . . . . . . 8 (𝑤 = 𝑧 → (𝑤‘1) = (𝑧‘1))
1110eqeq1d 2607 . . . . . . 7 (𝑤 = 𝑧 → ((𝑤‘1) = 𝑁 ↔ (𝑧‘1) = 𝑁))
1211elrab 3326 . . . . . 6 (𝑧 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁} ↔ (𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁))
1312a1i 11 . . . . 5 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁} ↔ (𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁)))
14 2nn0 11152 . . . . . . . . 9 2 ∈ ℕ0
15 frgrhash2wsp.v . . . . . . . . . 10 𝑉 = (Vtx‘𝐺)
1615wspthsnwspthsnon 41120 . . . . . . . . 9 ((2 ∈ ℕ0𝐺 ∈ FinUSGraph ) → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥𝑉𝑦𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦)))
1714, 16mpan 701 . . . . . . . 8 (𝐺 ∈ FinUSGraph → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥𝑉𝑦𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦)))
1817adantr 479 . . . . . . 7 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥𝑉𝑦𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦)))
19 fusgrusgr 40539 . . . . . . . . . 10 (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )
2019adantr 479 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → 𝐺 ∈ USGraph )
21 eqid 2605 . . . . . . . . . 10 (Edg‘𝐺) = (Edg‘𝐺)
2215, 21usgr2wspthon 41166 . . . . . . . . 9 ((𝐺 ∈ USGraph ∧ (𝑥𝑉𝑦𝑉)) → (𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
2320, 22sylan 486 . . . . . . . 8 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (𝑥𝑉𝑦𝑉)) → (𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
24232rexbidva 3033 . . . . . . 7 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (∃𝑥𝑉𝑦𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
2518, 24bitrd 266 . . . . . 6 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
2625anbi1d 736 . . . . 5 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁)))
27 19.41vv 1900 . . . . . . 7 (∃𝑥𝑦((𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥𝑦(𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁))
28 velsn 4136 . . . . . . . . . . . . 13 (𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)
2928bicomi 212 . . . . . . . . . . . 12 (𝑧 = ⟨“𝑥𝑁𝑦”⟩ ↔ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})
3029anbi2i 725 . . . . . . . . . . 11 (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
3130anbi2i 725 . . . . . . . . . 10 ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) ↔ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
3231a1i 11 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) ↔ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))))
33 fveq1 6083 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → (𝑧‘1) = (⟨“𝑥𝑚𝑦”⟩‘1))
34 vex 3171 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑚 ∈ V
35 s3fv1 13429 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 ∈ V → (⟨“𝑥𝑚𝑦”⟩‘1) = 𝑚)
3634, 35ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⟨“𝑥𝑚𝑦”⟩‘1) = 𝑚
3733, 36syl6eq 2655 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → (𝑧‘1) = 𝑚)
3837eqeq1d 2607 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
3938biimpd 217 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
4039adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) → ((𝑧‘1) = 𝑁𝑚 = 𝑁))
4140com12 32 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧‘1) = 𝑁 → ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) → 𝑚 = 𝑁))
4241ad2antlr 758 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ 𝑚𝑉) → ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) → 𝑚 = 𝑁))
4342imp 443 . . . . . . . . . . . . . . . . . . . 20 (((((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ 𝑚𝑉) ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦)) → 𝑚 = 𝑁)
44 preq1 4207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑚 = 𝑁 → {𝑚, 𝑦} = {𝑁, 𝑦})
45 prcom 4206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 {𝑁, 𝑦} = {𝑦, 𝑁}
4644, 45syl6eq 2655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑚 = 𝑁 → {𝑚, 𝑦} = {𝑦, 𝑁})
4746eleq1d 2667 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 = 𝑁 → ({𝑚, 𝑦} ∈ (Edg‘𝐺) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
4847biimpd 217 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 = 𝑁 → ({𝑚, 𝑦} ∈ (Edg‘𝐺) → {𝑦, 𝑁} ∈ (Edg‘𝐺)))
4948adantld 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 = 𝑁 → (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)) → {𝑦, 𝑁} ∈ (Edg‘𝐺)))
5049imp 443 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 = 𝑁 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → {𝑦, 𝑁} ∈ (Edg‘𝐺))
51503adant2 1072 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚 = 𝑁 ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → {𝑦, 𝑁} ∈ (Edg‘𝐺))
52 nesym 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥𝑦 ↔ ¬ 𝑦 = 𝑥)
5352biimpi 204 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝑦 → ¬ 𝑦 = 𝑥)
5453adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) → ¬ 𝑦 = 𝑥)
55543ad2ant2 1075 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚 = 𝑁 ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ¬ 𝑦 = 𝑥)
5651, 55jca 552 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 = 𝑁 ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))
57 preq2 4208 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 = 𝑁 → {𝑥, 𝑚} = {𝑥, 𝑁})
5857eleq1d 2667 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 = 𝑁 → ({𝑥, 𝑚} ∈ (Edg‘𝐺) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
5958biimpcd 237 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({𝑥, 𝑚} ∈ (Edg‘𝐺) → (𝑚 = 𝑁 → {𝑥, 𝑁} ∈ (Edg‘𝐺)))
6059adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)) → (𝑚 = 𝑁 → {𝑥, 𝑁} ∈ (Edg‘𝐺)))
6160impcom 444 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚 = 𝑁 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → {𝑥, 𝑁} ∈ (Edg‘𝐺))
62613adant2 1072 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 = 𝑁 ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → {𝑥, 𝑁} ∈ (Edg‘𝐺))
63 eqidd 2606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑚 = 𝑁𝑥 = 𝑥)
64 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑚 = 𝑁𝑚 = 𝑁)
65 eqidd 2606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑚 = 𝑁𝑦 = 𝑦)
6663, 64, 65s3eqd 13402 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑚 = 𝑁 → ⟨“𝑥𝑚𝑦”⟩ = ⟨“𝑥𝑁𝑦”⟩)
6766eqeq2d 2615 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 = 𝑁 → (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ↔ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))
6867biimpcd 237 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → (𝑚 = 𝑁𝑧 = ⟨“𝑥𝑁𝑦”⟩))
6968adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) → (𝑚 = 𝑁𝑧 = ⟨“𝑥𝑁𝑦”⟩))
7069impcom 444 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚 = 𝑁 ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦)) → 𝑧 = ⟨“𝑥𝑁𝑦”⟩)
71703adant3 1073 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑚 = 𝑁 ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → 𝑧 = ⟨“𝑥𝑁𝑦”⟩)
7256, 62, 71jca32 555 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 = 𝑁 ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
73723exp 1255 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑁 → ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) → (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))))
7473adantld 481 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑁 → (((((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ 𝑚𝑉) ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦)) → (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))))
7543, 74mpcom 37 . . . . . . . . . . . . . . . . . . 19 (((((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ 𝑚𝑉) ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦)) → (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
7675impr 646 . . . . . . . . . . . . . . . . . 18 (((((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ 𝑚𝑉) ∧ ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
7776a1d 25 . . . . . . . . . . . . . . . . 17 (((((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ 𝑚𝑉) ∧ ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
7877ex 448 . . . . . . . . . . . . . . . 16 ((((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) ∧ 𝑚𝑉) → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))))
7978rexlimdva 3008 . . . . . . . . . . . . . . 15 (((𝑥𝑉𝑦𝑉) ∧ (𝑧‘1) = 𝑁) → (∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))))
8079ex 448 . . . . . . . . . . . . . 14 ((𝑥𝑉𝑦𝑉) → ((𝑧‘1) = 𝑁 → (∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))))
8180com23 83 . . . . . . . . . . . . 13 ((𝑥𝑉𝑦𝑉) → (∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ((𝑧‘1) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))))
8281impr 646 . . . . . . . . . . . 12 ((𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) → ((𝑧‘1) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))))
8382imp 443 . . . . . . . . . . 11 (((𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
8483com12 32 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (((𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
85 usgrumgr 40407 . . . . . . . . . . . . . . . . . . . . . 22 (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
8619, 85syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝐺 ∈ FinUSGraph → 𝐺 ∈ UMGraph )
8786adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → 𝐺 ∈ UMGraph )
8887anim1i 589 . . . . . . . . . . . . . . . . . . 19 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → (𝐺 ∈ UMGraph ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
8915, 21umgrpredgav 40370 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → (𝑥𝑉𝑁𝑉))
90 simpl 471 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑉𝑁𝑉) → 𝑥𝑉)
9188, 89, 903syl 18 . . . . . . . . . . . . . . . . . 18 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → 𝑥𝑉)
9291expcom 449 . . . . . . . . . . . . . . . . 17 ({𝑥, 𝑁} ∈ (Edg‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → 𝑥𝑉))
9392adantr 479 . . . . . . . . . . . . . . . 16 (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → 𝑥𝑉))
9493com12 32 . . . . . . . . . . . . . . 15 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → 𝑥𝑉))
9594adantld 481 . . . . . . . . . . . . . 14 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → 𝑥𝑉))
9695imp 443 . . . . . . . . . . . . 13 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → 𝑥𝑉)
9787anim1i 589 . . . . . . . . . . . . . . . . . 18 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → (𝐺 ∈ UMGraph ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
9815, 21umgrpredgav 40370 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ UMGraph ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → (𝑦𝑉𝑁𝑉))
99 simpl 471 . . . . . . . . . . . . . . . . . 18 ((𝑦𝑉𝑁𝑉) → 𝑦𝑉)
10097, 98, 993syl 18 . . . . . . . . . . . . . . . . 17 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → 𝑦𝑉)
101100expcom 449 . . . . . . . . . . . . . . . 16 ({𝑦, 𝑁} ∈ (Edg‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → 𝑦𝑉))
102101adantr 479 . . . . . . . . . . . . . . 15 (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → 𝑦𝑉))
103102adantr 479 . . . . . . . . . . . . . 14 ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → 𝑦𝑉))
104103impcom 444 . . . . . . . . . . . . 13 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → 𝑦𝑉)
10567biimprd 236 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑁 → (𝑧 = ⟨“𝑥𝑁𝑦”⟩ → 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
106105adantld 481 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑁 → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
107106adantld 481 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑁 → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
108107imp 443 . . . . . . . . . . . . . . . . . 18 ((𝑚 = 𝑁 ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → 𝑧 = ⟨“𝑥𝑚𝑦”⟩)
10952bicomi 212 . . . . . . . . . . . . . . . . . . . . 21 𝑦 = 𝑥𝑥𝑦)
110109biimpi 204 . . . . . . . . . . . . . . . . . . . 20 𝑦 = 𝑥𝑥𝑦)
111110ad2antlr 758 . . . . . . . . . . . . . . . . . . 19 ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → 𝑥𝑦)
112111adantl 480 . . . . . . . . . . . . . . . . . 18 ((𝑚 = 𝑁 ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → 𝑥𝑦)
11347biimprd 236 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑁 → ({𝑦, 𝑁} ∈ (Edg‘𝐺) → {𝑚, 𝑦} ∈ (Edg‘𝐺)))
114113adantrd 482 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑁 → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) → {𝑚, 𝑦} ∈ (Edg‘𝐺)))
11558biimprd 236 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑁 → ({𝑥, 𝑁} ∈ (Edg‘𝐺) → {𝑥, 𝑚} ∈ (Edg‘𝐺)))
116115adantrd 482 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑁 → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → {𝑥, 𝑚} ∈ (Edg‘𝐺)))
117114, 116anim12d 583 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑁 → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ({𝑚, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑥, 𝑚} ∈ (Edg‘𝐺))))
118117imp 443 . . . . . . . . . . . . . . . . . . 19 ((𝑚 = 𝑁 ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → ({𝑚, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑥, 𝑚} ∈ (Edg‘𝐺)))
119118ancomd 465 . . . . . . . . . . . . . . . . . 18 ((𝑚 = 𝑁 ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))
120108, 112, 119jca31 554 . . . . . . . . . . . . . . . . 17 ((𝑚 = 𝑁 ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))
121120ex 448 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑁 → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
122121adantl 480 . . . . . . . . . . . . . . 15 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ 𝑚 = 𝑁) → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
1231, 122rspcimedv 3279 . . . . . . . . . . . . . 14 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
124123imp 443 . . . . . . . . . . . . 13 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))
12596, 104, 124jca32 555 . . . . . . . . . . . 12 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → (𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
126 fveq1 6083 . . . . . . . . . . . . . . . . . . 19 (𝑧 = ⟨“𝑥𝑁𝑦”⟩ → (𝑧‘1) = (⟨“𝑥𝑁𝑦”⟩‘1))
127 s3fv1 13429 . . . . . . . . . . . . . . . . . . 19 (𝑁𝑉 → (⟨“𝑥𝑁𝑦”⟩‘1) = 𝑁)
128126, 127sylan9eqr 2661 . . . . . . . . . . . . . . . . . 18 ((𝑁𝑉𝑧 = ⟨“𝑥𝑁𝑦”⟩) → (𝑧‘1) = 𝑁)
129128expcom 449 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨“𝑥𝑁𝑦”⟩ → (𝑁𝑉 → (𝑧‘1) = 𝑁))
130129adantl 480 . . . . . . . . . . . . . . . 16 (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → (𝑁𝑉 → (𝑧‘1) = 𝑁))
131130adantl 480 . . . . . . . . . . . . . . 15 ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → (𝑁𝑉 → (𝑧‘1) = 𝑁))
132131com12 32 . . . . . . . . . . . . . 14 (𝑁𝑉 → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → (𝑧‘1) = 𝑁))
133132adantl 480 . . . . . . . . . . . . 13 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → (𝑧‘1) = 𝑁))
134133imp 443 . . . . . . . . . . . 12 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → (𝑧‘1) = 𝑁)
135125, 134jca 552 . . . . . . . . . . 11 (((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → ((𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁))
136135ex 448 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ((𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁)))
13784, 136impbid 200 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (((𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁) ↔ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
138 eldif 3545 . . . . . . . . . . 11 (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}))
13921nbusgreledg 40573 . . . . . . . . . . . . . 14 (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
14019, 139syl 17 . . . . . . . . . . . . 13 (𝐺 ∈ FinUSGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
141140adantr 479 . . . . . . . . . . . 12 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
142 velsn 4136 . . . . . . . . . . . . . 14 (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
143142a1i 11 . . . . . . . . . . . . 13 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥))
144143notbid 306 . . . . . . . . . . . 12 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (¬ 𝑦 ∈ {𝑥} ↔ ¬ 𝑦 = 𝑥))
145141, 144anbi12d 742 . . . . . . . . . . 11 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑦 ∈ (𝐺 NeighbVtx 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
146138, 145syl5bb 270 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
14721nbusgreledg 40573 . . . . . . . . . . . . 13 (𝐺 ∈ USGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
14819, 147syl 17 . . . . . . . . . . . 12 (𝐺 ∈ FinUSGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
149148adantr 479 . . . . . . . . . . 11 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
150149anbi1d 736 . . . . . . . . . 10 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}) ↔ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
151146, 150anbi12d 742 . . . . . . . . 9 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})) ↔ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))))
15232, 137, 1513bitr4d 298 . . . . . . . 8 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (((𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁) ↔ (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))))
1531522exbidv 1837 . . . . . . 7 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (∃𝑥𝑦((𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥𝑦(𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))))
15427, 153syl5bbr 272 . . . . . 6 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((∃𝑥𝑦(𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥𝑦(𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))))
155 df-rex 2897 . . . . . . . . 9 (∃𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ∃𝑦(𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
156155rexbii 3018 . . . . . . . 8 (∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ∃𝑥𝑉𝑦(𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
157 df-rex 2897 . . . . . . . 8 (∃𝑥𝑉𝑦(𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ↔ ∃𝑥(𝑥𝑉 ∧ ∃𝑦(𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
158 19.42v 1903 . . . . . . . . . 10 (∃𝑦(𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ↔ (𝑥𝑉 ∧ ∃𝑦(𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
159158bicomi 212 . . . . . . . . 9 ((𝑥𝑉 ∧ ∃𝑦(𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ↔ ∃𝑦(𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
160159exbii 1762 . . . . . . . 8 (∃𝑥(𝑥𝑉 ∧ ∃𝑦(𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ↔ ∃𝑥𝑦(𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
161156, 157, 1603bitri 284 . . . . . . 7 (∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ∃𝑥𝑦(𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
162161anbi1i 726 . . . . . 6 ((∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥𝑦(𝑥𝑉 ∧ (𝑦𝑉 ∧ ∃𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁))
163 df-rex 2897 . . . . . . 7 (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ ∃𝑥(𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ ∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
164 r19.42v 3068 . . . . . . . . 9 (∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})(𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}) ↔ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ ∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
165 df-rex 2897 . . . . . . . . 9 (∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})(𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}) ↔ ∃𝑦(𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
166164, 165bitr3i 264 . . . . . . . 8 ((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ ∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}) ↔ ∃𝑦(𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
167166exbii 1762 . . . . . . 7 (∃𝑥(𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ ∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}) ↔ ∃𝑥𝑦(𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
168163, 167bitri 262 . . . . . 6 (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ ∃𝑥𝑦(𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
169154, 162, 1683bitr4g 301 . . . . 5 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → ((∃𝑥𝑉𝑦𝑉𝑚𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
17013, 26, 1693bitrd 292 . . . 4 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
171 vex 3171 . . . . . . 7 𝑧 ∈ V
172 eleq1 2671 . . . . . . . 8 (𝑝 = 𝑧 → (𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
1731722rexbidv 3034 . . . . . . 7 (𝑝 = 𝑧 → (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
174171, 173elab 3314 . . . . . 6 (𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})
175174bicomi 212 . . . . 5 (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}})
176175a1i 11 . . . 4 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
1779, 170, 1763bitrd 292 . . 3 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑧 ∈ (𝑀𝑁) ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
178177eqrdv 2603 . 2 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑀𝑁) = {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}})
179 dfiunv2 4482 . 2 𝑥 ∈ (𝐺 NeighbVtx 𝑁) 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){⟨“𝑥𝑁𝑦”⟩} = {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}
180178, 179syl6eqr 2657 1 ((𝐺 ∈ FinUSGraph ∧ 𝑁𝑉) → (𝑀𝑁) = 𝑥 ∈ (𝐺 NeighbVtx 𝑁) 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){⟨“𝑥𝑁𝑦”⟩})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wex 1694  wcel 1975  {cab 2591  wne 2775  wrex 2892  {crab 2895  Vcvv 3168  cdif 3532  {csn 4120  {cpr 4122   ciun 4445  cmpt 4633  cfv 5786  (class class class)co 6523  1c1 9789  2c2 10913  0cn0 11135  ⟨“cs3 13380  Vtxcvtx 40227   UMGraph cumgr 40305  Edgcedga 40349   USGraph cusgr 40377   FinUSGraph cfusgr 40533   NeighbVtx cnbgr 40548   WSPathsN cwwspthsn 41029   WSPathsNOn cwwspthsnon 41030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-rep 4689  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-ac2 9141  ax-cnex 9844  ax-resscn 9845  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-mulcom 9852  ax-addass 9853  ax-mulass 9854  ax-distr 9855  ax-i2m1 9856  ax-1ne0 9857  ax-1rid 9858  ax-rnegex 9859  ax-rrecex 9860  ax-cnre 9861  ax-pre-lttri 9862  ax-pre-lttrn 9863  ax-pre-ltadd 9864  ax-pre-mulgt0 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-ifp 1006  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-ral 2896  df-rex 2897  df-reu 2898  df-rmo 2899  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-int 4401  df-iun 4447  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-se 4984  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-isom 5795  df-riota 6485  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-om 6931  df-1st 7032  df-2nd 7033  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-1o 7420  df-2o 7421  df-oadd 7424  df-er 7602  df-map 7719  df-pm 7720  df-en 7815  df-dom 7816  df-sdom 7817  df-fin 7818  df-card 8621  df-ac 8795  df-cda 8846  df-pnf 9928  df-mnf 9929  df-xr 9930  df-ltxr 9931  df-le 9932  df-sub 10115  df-neg 10116  df-nn 10864  df-2 10922  df-3 10923  df-n0 11136  df-z 11207  df-uz 11516  df-fz 12149  df-fzo 12286  df-hash 12931  df-word 13096  df-concat 13098  df-s1 13099  df-s2 13386  df-s3 13387  df-uhgr 40278  df-upgr 40306  df-umgr 40307  df-edga 40350  df-uspgr 40378  df-usgr 40379  df-fusgr 40534  df-nbgr 40552  df-1wlks 40798  df-wlks 40799  df-wlkson 40800  df-trls 40899  df-trlson 40900  df-pths 40921  df-spths 40922  df-pthson 40923  df-spthson 40924  df-wwlks 41031  df-wwlksn 41032  df-wwlksnon 41033  df-wspthsn 41034  df-wspthsnon 41035
This theorem is referenced by:  fusgreghash2wspv  41497
  Copyright terms: Public domain W3C validator