fusgr2wsp2nb - Mathbox for Alexander van der Vekens

	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 41498

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.

Step	Hyp	Ref	Expression
1		simpr 476	. . . . 5 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ 𝑉)
2		ovex 6577	. . . . . 6 ⊢ (2 WSPathsN 𝐺) ∈ V
3	2	rabex 4740	. . . . 5 ⊢ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁} ∈ V
4		eqeq2 2621	. . . . . . . 8 ⊢ (𝑎 = 𝑁 → ((𝑤‘1) = 𝑎 ↔ (𝑤‘1) = 𝑁))
5	4	rabbidv 3164	. . . . . . 7 ⊢ (𝑎 = 𝑁 → {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎} = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁})
6		fusgreg2wsp.m	. . . . . . 7 ⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})
7	5, 6	fvmptg 6189	. . . . . 6 ⊢ ((𝑁 ∈ 𝑉 ∧ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁} ∈ V) → (𝑀‘𝑁) = {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁})
8	7	eleq2d 2673	. . . . 5 ⊢ ((𝑁 ∈ 𝑉 ∧ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁} ∈ V) → (𝑧 ∈ (𝑀‘𝑁) ↔ 𝑧 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁}))
9	1, 3, 8	sylancl 693	. . . 4 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ (𝑀‘𝑁) ↔ 𝑧 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁}))
10		fveq1 6102	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → (𝑤‘1) = (𝑧‘1))
11	10	eqeq1d 2612	. . . . . . 7 ⊢ (𝑤 = 𝑧 → ((𝑤‘1) = 𝑁 ↔ (𝑧‘1) = 𝑁))
12	11	elrab 3331	. . . . . 6 ⊢ (𝑧 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁} ↔ (𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁))
13	12	a1i 11	. . . . 5 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁} ↔ (𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁)))
14		2nn0 11186	. . . . . . . . 9 ⊢ 2 ∈ ℕ₀
15		frgrhash2wsp.v	. . . . . . . . . 10 ⊢ 𝑉 = (Vtx‘𝐺)
16	15	wspthsnwspthsnon 41122	. . . . . . . . 9 ⊢ ((2 ∈ ℕ₀ ∧ 𝐺 ∈ FinUSGraph ) → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦)))
17	14, 16	mpan 702	. . . . . . . 8 ⊢ (𝐺 ∈ FinUSGraph → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦)))
18	17	adantr 480	. . . . . . 7 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦)))
19		fusgrusgr 40541	. . . . . . . . . 10 ⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )
20	19	adantr 480	. . . . . . . . 9 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → 𝐺 ∈ USGraph )
21		eqid 2610	. . . . . . . . . 10 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
22	15, 21	usgr2wspthon 41168	. . . . . . . . 9 ⊢ ((𝐺 ∈ USGraph ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
23	20, 22	sylan 487	. . . . . . . 8 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
24	23	2rexbidva 3038	. . . . . . 7 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 𝑧 ∈ (𝑥(2 WSPathsNOn 𝐺)𝑦) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
25	18, 24	bitrd 267	. . . . . 6 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
26	25	anbi1d 737	. . . . 5 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((𝑧 ∈ (2 WSPathsN 𝐺) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁)))
27		19.41vv 1902	. . . . . . 7 ⊢ (∃𝑥∃𝑦((𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥∃𝑦(𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁))
28		velsn 4141	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)
29	28	bicomi 213	. . . . . . . . . . . 12 ⊢ (𝑧 = ⟨“𝑥𝑁𝑦”⟩ ↔ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})
30	29	anbi2i 726	. . . . . . . . . . 11 ⊢ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) ↔ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
31	30	anbi2i 726	. . . . . . . . . 10 ⊢ ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) ↔ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
32	31	a1i 11	. . . . . . . . 9 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) ↔ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))))
33		fveq1 6102	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → (𝑧‘1) = (⟨“𝑥𝑚𝑦”⟩‘1))
34		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑚 ∈ V
35		s3fv1 13487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 ∈ V → (⟨“𝑥𝑚𝑦”⟩‘1) = 𝑚)
36	34, 35	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟨“𝑥𝑚𝑦”⟩‘1) = 𝑚
37	33, 36	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → (𝑧‘1) = 𝑚)
38	37	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → ((𝑧‘1) = 𝑁 ↔ 𝑚 = 𝑁))
39	38	biimpd 218	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → ((𝑧‘1) = 𝑁 → 𝑚 = 𝑁))
40	39	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) → ((𝑧‘1) = 𝑁 → 𝑚 = 𝑁))
41	40	com12 32	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧‘1) = 𝑁 → ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) → 𝑚 = 𝑁))
42	41	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ 𝑚 ∈ 𝑉) → ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) → 𝑚 = 𝑁))
43	42	imp 444	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ 𝑚 ∈ 𝑉) ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦)) → 𝑚 = 𝑁)
44		preq1 4212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑚 = 𝑁 → {𝑚, 𝑦} = {𝑁, 𝑦})
45		prcom 4211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ {𝑁, 𝑦} = {𝑦, 𝑁}
46	44, 45	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑚 = 𝑁 → {𝑚, 𝑦} = {𝑦, 𝑁})
47	46	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 = 𝑁 → ({𝑚, 𝑦} ∈ (Edg‘𝐺) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
48	47	biimpd 218	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 = 𝑁 → ({𝑚, 𝑦} ∈ (Edg‘𝐺) → {𝑦, 𝑁} ∈ (Edg‘𝐺)))
49	48	adantld 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 = 𝑁 → (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)) → {𝑦, 𝑁} ∈ (Edg‘𝐺)))
50	49	imp 444	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑚 = 𝑁 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → {𝑦, 𝑁} ∈ (Edg‘𝐺))
51	50	3adant2 1073	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑚 = 𝑁 ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → {𝑦, 𝑁} ∈ (Edg‘𝐺))
52		nesym 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑦 = 𝑥)
53	52	biimpi 205	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ≠ 𝑦 → ¬ 𝑦 = 𝑥)
54	53	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) → ¬ 𝑦 = 𝑥)
55	54	3ad2ant2 1076	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑚 = 𝑁 ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ¬ 𝑦 = 𝑥)
56	51, 55	jca 553	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 = 𝑁 ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥))
57		preq2 4213	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 = 𝑁 → {𝑥, 𝑚} = {𝑥, 𝑁})
58	57	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 = 𝑁 → ({𝑥, 𝑚} ∈ (Edg‘𝐺) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
59	58	biimpcd 238	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({𝑥, 𝑚} ∈ (Edg‘𝐺) → (𝑚 = 𝑁 → {𝑥, 𝑁} ∈ (Edg‘𝐺)))
60	59	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)) → (𝑚 = 𝑁 → {𝑥, 𝑁} ∈ (Edg‘𝐺)))
61	60	impcom 445	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑚 = 𝑁 ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → {𝑥, 𝑁} ∈ (Edg‘𝐺))
62	61	3adant2 1073	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 = 𝑁 ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → {𝑥, 𝑁} ∈ (Edg‘𝐺))
63		eqidd 2611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑚 = 𝑁 → 𝑥 = 𝑥)
64		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑚 = 𝑁 → 𝑚 = 𝑁)
65		eqidd 2611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑚 = 𝑁 → 𝑦 = 𝑦)
66	63, 64, 65	s3eqd 13460	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 = 𝑁 → ⟨“𝑥𝑚𝑦”⟩ = ⟨“𝑥𝑁𝑦”⟩)
67	66	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 = 𝑁 → (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ↔ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))
68	67	biimpcd 238	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ → (𝑚 = 𝑁 → 𝑧 = ⟨“𝑥𝑁𝑦”⟩))
69	68	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) → (𝑚 = 𝑁 → 𝑧 = ⟨“𝑥𝑁𝑦”⟩))
70	69	impcom 445	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑚 = 𝑁 ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦)) → 𝑧 = ⟨“𝑥𝑁𝑦”⟩)
71	70	3adant3 1074	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 = 𝑁 ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → 𝑧 = ⟨“𝑥𝑁𝑦”⟩)
72	56, 62, 71	jca32 556	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = 𝑁 ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
73	72	3exp 1256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑁 → ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) → (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))))
74	73	adantld 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑁 → (((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ 𝑚 ∈ 𝑉) ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦)) → (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))))
75	43, 74	mpcom 37	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ 𝑚 ∈ 𝑉) ∧ (𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦)) → (({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
76	75	impr 647	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ 𝑚 ∈ 𝑉) ∧ ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))
77	76	a1d 25	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ 𝑚 ∈ 𝑉) ∧ ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
78	77	ex 449	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) ∧ 𝑚 ∈ 𝑉) → (((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))))
79	78	rexlimdva 3013	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (𝑧‘1) = 𝑁) → (∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))))
80	79	ex 449	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝑧‘1) = 𝑁 → (∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))))
81	80	com23 84	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) → ((𝑧‘1) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))))
82	81	impr 647	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) → ((𝑧‘1) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)))))
83	82	imp 444	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
84	83	com12 32	. . . . . . . . . 10 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (((𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁) → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
85		usgrumgr 40409	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
86	19, 85	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ UMGraph )
87	86	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → 𝐺 ∈ UMGraph )
88	87	anim1i 590	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → (𝐺 ∈ UMGraph ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
89	15, 21	umgrpredgav 25813	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ UMGraph ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → (𝑥 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
90		simpl 472	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → 𝑥 ∈ 𝑉)
91	88, 89, 90	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ {𝑥, 𝑁} ∈ (Edg‘𝐺)) → 𝑥 ∈ 𝑉)
92	91	expcom 450	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑥, 𝑁} ∈ (Edg‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑥 ∈ 𝑉))
93	92	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑥 ∈ 𝑉))
94	93	com12 32	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → 𝑥 ∈ 𝑉))
95	94	adantld 482	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → 𝑥 ∈ 𝑉))
96	95	imp 444	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → 𝑥 ∈ 𝑉)
97	87	anim1i 590	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → (𝐺 ∈ UMGraph ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
98	15, 21	umgrpredgav 25813	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ UMGraph ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → (𝑦 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))
99		simpl 472	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → 𝑦 ∈ 𝑉)
100	97, 98, 99	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ {𝑦, 𝑁} ∈ (Edg‘𝐺)) → 𝑦 ∈ 𝑉)
101	100	expcom 450	. . . . . . . . . . . . . . . 16 ⊢ ({𝑦, 𝑁} ∈ (Edg‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑦 ∈ 𝑉))
102	101	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑦 ∈ 𝑉))
103	102	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑦 ∈ 𝑉))
104	103	impcom 445	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → 𝑦 ∈ 𝑉)
105	67	biimprd 237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑁 → (𝑧 = ⟨“𝑥𝑁𝑦”⟩ → 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
106	105	adantld 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑁 → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
107	106	adantld 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑁 → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → 𝑧 = ⟨“𝑥𝑚𝑦”⟩))
108	107	imp 444	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 = 𝑁 ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → 𝑧 = ⟨“𝑥𝑚𝑦”⟩)
109	52	bicomi 213	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ 𝑦 = 𝑥 ↔ 𝑥 ≠ 𝑦)
110	109	biimpi 205	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑦 = 𝑥 → 𝑥 ≠ 𝑦)
111	110	ad2antlr 759	. . . . . . . . . . . . . . . . . . 19 ⊢ ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → 𝑥 ≠ 𝑦)
112	111	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 = 𝑁 ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → 𝑥 ≠ 𝑦)
113	47	biimprd 237	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑁 → ({𝑦, 𝑁} ∈ (Edg‘𝐺) → {𝑚, 𝑦} ∈ (Edg‘𝐺)))
114	113	adantrd 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑁 → (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) → {𝑚, 𝑦} ∈ (Edg‘𝐺)))
115	58	biimprd 237	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑁 → ({𝑥, 𝑁} ∈ (Edg‘𝐺) → {𝑥, 𝑚} ∈ (Edg‘𝐺)))
116	115	adantrd 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑁 → (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → {𝑥, 𝑚} ∈ (Edg‘𝐺)))
117	114, 116	anim12d 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑁 → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ({𝑚, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑥, 𝑚} ∈ (Edg‘𝐺))))
118	117	imp 444	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 = 𝑁 ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → ({𝑚, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑥, 𝑚} ∈ (Edg‘𝐺)))
119	118	ancomd 466	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 = 𝑁 ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))
120	108, 112, 119	jca31 555	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 = 𝑁 ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))
121	120	ex 449	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑁 → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
122	121	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑚 = 𝑁) → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
123	1, 122	rspcimedv 3284	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
124	123	imp 444	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))
125	96, 104, 124	jca32 556	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → (𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
126		fveq1 6102	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ⟨“𝑥𝑁𝑦”⟩ → (𝑧‘1) = (⟨“𝑥𝑁𝑦”⟩‘1))
127		s3fv1 13487	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ 𝑉 → (⟨“𝑥𝑁𝑦”⟩‘1) = 𝑁)
128	126, 127	sylan9eqr 2666	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → (𝑧‘1) = 𝑁)
129	128	expcom 450	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ⟨“𝑥𝑁𝑦”⟩ → (𝑁 ∈ 𝑉 → (𝑧‘1) = 𝑁))
130	129	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩) → (𝑁 ∈ 𝑉 → (𝑧‘1) = 𝑁))
131	130	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → (𝑁 ∈ 𝑉 → (𝑧‘1) = 𝑁))
132	131	com12 32	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ 𝑉 → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → (𝑧‘1) = 𝑁))
133	132	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → (𝑧‘1) = 𝑁))
134	133	imp 444	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → (𝑧‘1) = 𝑁)
135	125, 134	jca 553	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) ∧ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))) → ((𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁))
136	135	ex 449	. . . . . . . . . 10 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩)) → ((𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁)))
137	84, 136	impbid 201	. . . . . . . . 9 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (((𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁) ↔ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 = ⟨“𝑥𝑁𝑦”⟩))))
138		eldif 3550	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ↔ (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}))
139	21	nbusgreledg 40575	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
140	19, 139	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ FinUSGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
141	140	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑦 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑦, 𝑁} ∈ (Edg‘𝐺)))
142		velsn 4141	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
143	142	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥))
144	143	notbid 307	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (¬ 𝑦 ∈ {𝑥} ↔ ¬ 𝑦 = 𝑥))
145	141, 144	anbi12d 743	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((𝑦 ∈ (𝐺 NeighbVtx 𝑁) ∧ ¬ 𝑦 ∈ {𝑥}) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
146	138, 145	syl5bb 271	. . . . . . . . . 10 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ↔ ({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥)))
147	21	nbusgreledg 40575	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ USGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
148	19, 147	syl 17	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ FinUSGraph → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
149	148	adantr 480	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ↔ {𝑥, 𝑁} ∈ (Edg‘𝐺)))
150	149	anbi1d 737	. . . . . . . . . 10 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}) ↔ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
151	146, 150	anbi12d 743	. . . . . . . . 9 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})) ↔ (({𝑦, 𝑁} ∈ (Edg‘𝐺) ∧ ¬ 𝑦 = 𝑥) ∧ ({𝑥, 𝑁} ∈ (Edg‘𝐺) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))))
152	32, 137, 151	3bitr4d 299	. . . . . . . 8 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (((𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁) ↔ (𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))))
153	152	2exbidv 1839	. . . . . . 7 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (∃𝑥∃𝑦((𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥∃𝑦(𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))))
154	27, 153	syl5bbr 273	. . . . . 6 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((∃𝑥∃𝑦(𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥∃𝑦(𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))))
155		df-rex 2902	. . . . . . . . 9 ⊢ (∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ∃𝑦(𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
156	155	rexbii 3023	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦(𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))))
157		df-rex 2902	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝑉 ∃𝑦(𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺)))) ↔ ∃𝑥(𝑥 ∈ 𝑉 ∧ ∃𝑦(𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
158		19.42v 1905	. . . . . . . . . 10 ⊢ (∃𝑦(𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ↔ (𝑥 ∈ 𝑉 ∧ ∃𝑦(𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
159	158	bicomi 213	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑉 ∧ ∃𝑦(𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ↔ ∃𝑦(𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
160	159	exbii 1764	. . . . . . . 8 ⊢ (∃𝑥(𝑥 ∈ 𝑉 ∧ ∃𝑦(𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
161	156, 157, 160	3bitri 285	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))))
162	161	anbi1i 727	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁) ↔ (∃𝑥∃𝑦(𝑥 ∈ 𝑉 ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))))) ∧ (𝑧‘1) = 𝑁))
163		df-rex 2902	. . . . . . 7 ⊢ (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ ∃𝑥(𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ ∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
164		r19.42v 3073	. . . . . . . . 9 ⊢ (∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})(𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}) ↔ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ ∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
165		df-rex 2902	. . . . . . . . 9 ⊢ (∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})(𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}) ↔ ∃𝑦(𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
166	164, 165	bitr3i 265	. . . . . . . 8 ⊢ ((𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ ∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}) ↔ ∃𝑦(𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
167	166	exbii 1764	. . . . . . 7 ⊢ (∃𝑥(𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ ∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}) ↔ ∃𝑥∃𝑦(𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
168	163, 167	bitri 263	. . . . . 6 ⊢ (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ ∃𝑥∃𝑦(𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}) ∧ (𝑥 ∈ (𝐺 NeighbVtx 𝑁) ∧ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})))
169	154, 162, 168	3bitr4g 302	. . . . 5 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → ((∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑚 ∈ 𝑉 ((𝑧 = ⟨“𝑥𝑚𝑦”⟩ ∧ 𝑥 ≠ 𝑦) ∧ ({𝑥, 𝑚} ∈ (Edg‘𝐺) ∧ {𝑚, 𝑦} ∈ (Edg‘𝐺))) ∧ (𝑧‘1) = 𝑁) ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
170	13, 26, 169	3bitrd 293	. . . 4 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑁} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
171		vex 3176	. . . . . . 7 ⊢ 𝑧 ∈ V
172		eleq1 2676	. . . . . . . 8 ⊢ (𝑝 = 𝑧 → (𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
173	172	2rexbidv 3039	. . . . . . 7 ⊢ (𝑝 = 𝑧 → (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩}))
174	171, 173	elab 3319	. . . . . 6 ⊢ (𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}} ↔ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩})
175	174	bicomi 213	. . . . 5 ⊢ (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}})
176	175	a1i 11	. . . 4 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑧 ∈ {⟨“𝑥𝑁𝑦”⟩} ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
177	9, 170, 176	3bitrd 293	. . 3 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑧 ∈ (𝑀‘𝑁) ↔ 𝑧 ∈ {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}))
178	177	eqrdv 2608	. 2 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑀‘𝑁) = {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}})
179		dfiunv2 4492	. 2 ⊢ ∪ 𝑥 ∈ (𝐺 NeighbVtx 𝑁)∪ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){⟨“𝑥𝑁𝑦”⟩} = {𝑝 ∣ ∃𝑥 ∈ (𝐺 NeighbVtx 𝑁)∃𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥})𝑝 ∈ {⟨“𝑥𝑁𝑦”⟩}}
180	178, 179	syl6eqr 2662	1 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑀‘𝑁) = ∪ 𝑥 ∈ (𝐺 NeighbVtx 𝑁)∪ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){⟨“𝑥𝑁𝑦”⟩})

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∃wex 1695 ∈ wcel 1977 {cab 2596 ≠ wne 2780 ∃wrex 2897 {crab 2900 Vcvv 3173 ∖ cdif 3537 {csn 4125 {cpr 4127 ∪ ciun 4455 ↦ cmpt 4643 ‘cfv 5804 (class class class)co 6549 1c1 9816 2c2 10947 ℕ₀cn0 11169 ⟨“cs3 13438 Vtxcvtx 25673 UMGraph cumgr 25748 Edgcedga 25792 USGraph cusgr 40379 FinUSGraph cfusgr 40535 NeighbVtx cnbgr 40550 WSPathsN cwwspthsn 41031 WSPathsNOn cwwspthsnon 41032

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-ac2 9168 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-ifp 1007 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-ac 8822 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-z 11255 df-uz 11564 df-fz 12198 df-fzo 12335 df-hash 12980 df-word 13154 df-concat 13156 df-s1 13157 df-s2 13444 df-s3 13445 df-uhgr 25724 df-upgr 25749 df-umgr 25750 df-edga 25793 df-uspgr 40380 df-usgr 40381 df-fusgr 40536 df-nbgr 40554 df-1wlks 40800 df-wlks 40801 df-wlkson 40802 df-trls 40901 df-trlson 40902 df-pths 40923 df-spths 40924 df-pthson 40925 df-spthson 40926 df-wwlks 41033 df-wwlksn 41034 df-wwlksnon 41035 df-wspthsn 41036 df-wspthsnon 41037

This theorem is referenced by: fusgreghash2wspv 41499

W3C validator