Theorem fusgr2wsp2nb 30962

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.

Step	Hyp	Ref	Expression
1		frgrhash2wsp.v	. . . . . 6 ⊢ 𝑉 = (Vtx‘𝐺)
2		fusgreg2wsp.m	. . . . . 6 ⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})
3	1, 2	fusgreg2wsplem 30961	. . . . 5 ⊢ (𝑁 ∈ 𝑉 → (𝑧 ∈ (𝑀‘𝑁) ↔ (𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁)))
4	3	adantl 487	. . . 4 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ (𝑀‘𝑁) ↔ (𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁)))
5	1	wspthsnwspthsnon 30532	. . . . . . 7 ⊢ (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦))
6		fusgrusgr 29930	. . . . . . . . . 10 ⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph)
7	6	adantr 486	. . . . . . . . 9 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → 𝐺 ∈ USGraph)
8		eqid 2763	. . . . . . . . . 10 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
9	1, 8	usgr2wspthon 30584	. . . . . . . . 9 ⊢ ((𝐺 ∈ USGraph ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
10	7, 9	sylan 592	. . . . . . . 8 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
11	10	2rexbidva 3229	. . . . . . 7 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
12	5, 11	bitrid 286	. . . . . 6 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
13	12	anbi1d 643	. . . . 5 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁)))
14		19.41vv 1985	. . . . . . 7 ⊢ (∃𝑥∃𝑦(((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥∃𝑦((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁))
15		velsn 4600	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)
16	15	bicomi 227	. . . . . . . . . . 11 ⊢ (𝑧 = ⟨“𝑥𝑁𝑦”⟩ ↔ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})
17	16	anbi2i 635	. . . . . . . . . 10 ⊢ ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
18	17	a1i 11	. . . . . . . . 9 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
19		simplr 781	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁)) → 𝑁 ∈ 𝑉)
20		anass 474	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ (𝑥 ≠ 𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
21		ancom 466	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ (𝑥 ≠ 𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ↔ ((𝑥 ≠ 𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
22		an12 658	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ≠ 𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ (𝑥 ≠ 𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))
23		nesym 3015	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑦 = 𝑥)
24		prcom 4693	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑚, 𝑦} = {𝑦, 𝑚}
25	24	eleq1i 2855	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑚, 𝑦} ∈ (Edg‘𝐺) ↔ {𝑦, 𝑚} ∈ (Edg‘𝐺))
26	23, 25	anbi12ci 641	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ≠ 𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)) ↔ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))
27	26	anbi2i 635	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ (𝑥 ≠ 𝑦 ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
28	22, 27	bitri 278	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ≠ 𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
29	28	anbi1i 636	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ≠ 𝑦 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩) ↔ (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
30	20, 21, 29	3bitri 300	. . . . . . . . . . . . . 14 ⊢ (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
31		preq2 4695	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑁 → {𝑥, 𝑚} = {𝑥, 𝑁})
32	31	eleq1d 2849	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑁 → ({𝑥, 𝑚} ∈ (Edg‘𝐺) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
33		preq2 4695	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑁 → {𝑦, 𝑚} = {𝑦, 𝑁})
34	33	eleq1d 2849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑁 → ({𝑦, 𝑚} ∈ (Edg‘𝐺) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
35	34	anbi1d 643	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑁 → (({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
36	32, 35	anbi12d 644	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑁 → (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ↔ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))))
37		s3eq2 15046	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑁 → ⟨“𝑥𝑚𝑦”⟩ = ⟨“𝑥𝑁𝑦”⟩)
38	37	eqeq2d 2774	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑁 → (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ↔ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))
39	36, 38	anbi12d 644	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑁 → ((({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑚} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑚𝑦”⟩) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
40	30, 39	bitrid 286	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑁 → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
41	40	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁)) ∧ 𝑚 = 𝑁) → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
42		fveq1 6904	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → (𝑧‘1) = (⟨“𝑥𝑚𝑦”⟩‘1))
43		s3fv1 15069	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ V → (⟨“𝑥𝑚𝑦”⟩‘1) = 𝑚)
44	43	elv 3459	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨“𝑥𝑚𝑦”⟩‘1) = 𝑚
45	42, 44	eqtrdi 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → (𝑧‘1) = 𝑚)
46	45	eqeq1d 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → ((𝑧‘1) = 𝑁 ↔ 𝑚 = 𝑁))
47	46	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → ((𝑧‘1) = 𝑁 → 𝑚 = 𝑁))
48	47	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) → ((𝑧‘1) = 𝑁 → 𝑚 = 𝑁))
49	48	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ((𝑧‘1) = 𝑁 → 𝑚 = 𝑁))
50	49	com12 33	. . . . . . . . . . . . . 14 ⊢ ((𝑧‘1) = 𝑁 → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → 𝑚 = 𝑁))
51	50	ad2antll 742	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁)) → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → 𝑚 = 𝑁))
52	51	imp 412	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁)) ∧ ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) → 𝑚 = 𝑁)
53	19, 41, 52	rspcebdv 3574	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁)) → (∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
54	53	pm5.32da 590	. . . . . . . . . 10 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ↔ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
55		an32 659	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
56	55	a1i 11	. . . . . . . . . 10 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
57		usgrumgr 29789	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph)
58	1, 8	umgrpredgv 29745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → (𝑥 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
59	58	simpld 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → 𝑥 ∈ 𝑉)
60	59	ex 418	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺 ∈ UMGraph → ({𝑥, 𝑁} ∈ (Edg‘𝐺) → 𝑥 ∈ 𝑉))
61	1, 8	umgrpredgv 29745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 ∈ UMGraph ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → (𝑦 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
62	61	simpld 500	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺 ∈ UMGraph ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → 𝑦 ∈ 𝑉)
63	62	expcom 419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑦, 𝑁} ∈ (Edg‘𝐺) → (𝐺 ∈ UMGraph → 𝑦 ∈ 𝑉))
64	63	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) → (𝐺 ∈ UMGraph → 𝑦 ∈ 𝑉))
65	64	com12 33	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺 ∈ UMGraph → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ 𝑉))
66	60, 65	anim12d 621	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ UMGraph → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)))
67	6, 57, 66	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 ∈ FinUSGraph → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)))
68	67	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)))
69	68	com12 33	. . . . . . . . . . . . . . 15 ⊢ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)))
70	69	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)))
71	70	impcom 413	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))
72		fveq1 6904	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ⟨“𝑥𝑁𝑦”⟩ → (𝑧‘1) = (⟨“𝑥𝑁𝑦”⟩‘1))
73	72	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → (𝑧‘1) = (⟨“𝑥𝑁𝑦”⟩‘1))
74		s3fv1 15069	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ 𝑉 → (⟨“𝑥𝑁𝑦”⟩‘1) = 𝑁)
75	74	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (⟨“𝑥𝑁𝑦”⟩‘1) = 𝑁)
76	73, 75	sylan9eqr 2820	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → (𝑧‘1) = 𝑁)
77	71, 76	jca 521	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁))
78	77	ex 418	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁)))
79	78	pm4.71rd 572	. . . . . . . . . 10 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
80	54, 56, 79	3bitr4d 314	. . . . . . . . 9 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
81	8	nbusgreledg 29961	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ USGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
82	6, 81	syl 18	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ FinUSGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
83	82	adantr 486	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
84		eldif 4052	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}))
85	8	nbusgreledg 29961	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
86	6, 85	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ FinUSGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
87	86	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
88		velsn 4600	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
89	88	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥))
90	89	notbid 321	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (¬ 𝑦 ∈ {𝑥} ↔ ¬ 𝑦 = 𝑥))
91	87, 90	anbi12d 644	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((𝑦 ∈ (𝐺 NeighbVtx 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
92	84, 91	bitrid 286	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
93	83, 92	anbi12d 644	. . . . . . . . . 10 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ↔ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))))
94	93	anbi1d 643	. . . . . . . . 9 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}) ↔ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
95	18, 80, 94	3bitr4d 314	. . . . . . . 8 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
96	95	2exbidv 1959	. . . . . . 7 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (∃𝑥∃𝑦(((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥∃𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
97	14, 96	bitr3id 288	. . . . . 6 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((∃𝑥∃𝑦((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥∃𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
98		r2ex 3203	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
99	98	anbi1i 636	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥∃𝑦((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ∧ (𝑧‘1) = 𝑁))
100		r2ex 3203	. . . . . 6 ⊢ (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ ∃𝑥∃𝑦((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
101	97, 99, 100	3bitr4g 317	. . . . 5 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
102		vex 3458	. . . . . . . 8 ⊢ 𝑧 ∈ V
103		eleq1w 2847	. . . . . . . . 9 ⊢ (𝑝 = 𝑧 → (𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
104	103	2rexbidv 3231	. . . . . . . 8 ⊢ (𝑝 = 𝑧 → (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
105	102, 104	elab 3636	. . . . . . 7 ⊢ (𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})
106	105	bicomi 227	. . . . . 6 ⊢ (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}})
107	106	a1i 11	. . . . 5 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
108	13, 101, 107	3bitrd 308	. . . 4 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁) ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
109	4, 108	bitrd 282	. . 3 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ (𝑀‘𝑁) ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
110	109	eqrdv 2761	. 2 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑀‘𝑁) = {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}})
111		dfiunv2 4995	. 2 ⊢ ∪ 𝑥 ∈ (𝐺 NeighbVtx 𝑁)∪ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){⟨“𝑥𝑁𝑦”⟩} = {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}
112	110, 111	eqtr4di 2816	1 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑀‘𝑁) = ∪ 𝑥 ∈ (𝐺 NeighbVtx 𝑁)∪ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){⟨“𝑥𝑁𝑦”⟩})

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2147  {cab 2741   ≠ wne 2959  ∃wrex 3090  {crab 3416  Vcvv 3454   ∖ cdif 4048  {csn 4588  {cpr 4590  ∪ ciun 4954   ↦ cmpt 5189  ‘cfv 6555  (class class class)co 7440  1c1 11225  2c2 12421  ⟨“cs3 15018  Vtxcvtx 29601  Edgcedg 29652  UMGraphcumgr 29686  USGraphcusgr 29757  FinUSGraphcfusgr 29924   NeighbVtx cnbgr 29940   WSPathsN cwwspthsn 30444   WSPathsNOn cwwspthsnon 30445

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-cnex 11280  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300  ax-pre-mulgt0 11301

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ifp 1079  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-riota 7397  df-ov 7443  df-oprab 7444  df-mpo 7445  df-om 7899  df-1st 8022  df-2nd 8023  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443  df-1o 8501  df-2o 8502  df-oadd 8505  df-er 8742  df-map 8874  df-pm 8875  df-en 8999  df-dom 9000  df-sdom 9001  df-fin 9002  df-dju 10006  df-card 10044  df-pnf 11369  df-mnf 11370  df-xr 11371  df-ltxr 11372  df-le 11373  df-sub 11567  df-neg 11568  df-nn 12360  df-2 12429  df-3 12430  df-n0 12631  df-xnn0 12704  df-z 12718  df-uz 12990  df-fz 13664  df-fzo 13813  df-hash 14499  df-word 14683  df-concat 14740  df-s1 14767  df-s2 15024  df-s3 15025  df-edg 29653  df-uhgr 29663  df-upgr 29687  df-umgr 29688  df-uspgr 29758  df-usgr 29759  df-fusgr 29925  df-nbgr 29941  df-wlks 30207  df-wlkson 30208  df-trls 30302  df-trlson 30303  df-pths 30326  df-spths 30327  df-pthson 30328  df-spthson 30329  df-wwlks 30446  df-wwlksn 30447  df-wwlksnon 30448  df-wspthsn 30449  df-wspthsnon 30450

This theorem is used by:  fusgreghash2wspv  30963