Metamath Proof Explorer

Theorem fusgr2wsp2nb

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)

Ref Expression
Hypotheses frgrhash2wsp.v ⊢ V = Vtx ⁡ G
fusgreg2wsp.m ⊢ M = a ∈ V ⟼ w ∈ 2 WSPathsN G | w ⁡ 1 = a
Assertion fusgr2wsp2nb ⊢ G ∈ FinUSGraph ∧ N ∈ V → M ⁡ N = ⋃ x ∈ G NeighbVtx N ⋃ y ∈ G NeighbVtx N ∖ x ⟨“ xNy ”⟩

Proof

Step Hyp Ref Expression
1 frgrhash2wsp.v ⊢ V = Vtx ⁡ G
2 fusgreg2wsp.m ⊢ M = a ∈ V ⟼ w ∈ 2 WSPathsN G | w ⁡ 1 = a
3 1 2 fusgreg2wsplem ⊢ N ∈ V → z ∈ M ⁡ N ↔ z ∈ 2 WSPathsN G ∧ z ⁡ 1 = N
4 3 adantl ⊢ G ∈ FinUSGraph ∧ N ∈ V → z ∈ M ⁡ N ↔ z ∈ 2 WSPathsN G ∧ z ⁡ 1 = N
5 1 wspthsnwspthsnon ⊢ z ∈ 2 WSPathsN G ↔ ∃ x ∈ V ∃ y ∈ V z ∈ x 2 WSPathsNOn G y
6 fusgrusgr ⊢ G ∈ FinUSGraph → G ∈ USGraph
7 6 adantr ⊢ G ∈ FinUSGraph ∧ N ∈ V → G ∈ USGraph
8 eqid ⊢ Edg ⁡ G = Edg ⁡ G
9 1 8 usgr2wspthon ⊢ G ∈ USGraph ∧ x ∈ V ∧ y ∈ V → z ∈ x 2 WSPathsNOn G y ↔ ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G
10 7 9 sylan ⊢ G ∈ FinUSGraph ∧ N ∈ V ∧ x ∈ V ∧ y ∈ V → z ∈ x 2 WSPathsNOn G y ↔ ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G
11 10 2rexbidva ⊢ G ∈ FinUSGraph ∧ N ∈ V → ∃ x ∈ V ∃ y ∈ V z ∈ x 2 WSPathsNOn G y ↔ ∃ x ∈ V ∃ y ∈ V ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G
12 5 11 syl5bb ⊢ G ∈ FinUSGraph ∧ N ∈ V → z ∈ 2 WSPathsN G ↔ ∃ x ∈ V ∃ y ∈ V ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G
13 12 anbi1d ⊢ G ∈ FinUSGraph ∧ N ∈ V → z ∈ 2 WSPathsN G ∧ z ⁡ 1 = N ↔ ∃ x ∈ V ∃ y ∈ V ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ∧ z ⁡ 1 = N
14 19.41vv ⊢ ∃ x ∃ y x ∈ V ∧ y ∈ V ∧ ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ∧ z ⁡ 1 = N ↔ ∃ x ∃ y x ∈ V ∧ y ∈ V ∧ ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ∧ z ⁡ 1 = N
15 velsn ⊢ z ∈ ⟨“ xNy ”⟩ ↔ z = ⟨“ xNy ”⟩
16 15 bicomi ⊢ z = ⟨“ xNy ”⟩ ↔ z ∈ ⟨“ xNy ”⟩
17 16 anbi2i ⊢ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xNy ”⟩ ↔ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z ∈ ⟨“ xNy ”⟩
18 17 a1i ⊢ G ∈ FinUSGraph ∧ N ∈ V → x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xNy ”⟩ ↔ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z ∈ ⟨“ xNy ”⟩
19 simplr ⊢ G ∈ FinUSGraph ∧ N ∈ V ∧ x ∈ V ∧ y ∈ V ∧ z ⁡ 1 = N → N ∈ V
20 anass ⊢ z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ↔ z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G
21 ancom ⊢ z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ↔ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ∧ z = ⟨“ xmy ”⟩
22 an12 ⊢ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ↔ x m ∈ Edg ⁡ G ∧ x ≠ y ∧ m y ∈ Edg ⁡ G
23 nesym ⊢ x ≠ y ↔ ¬ y = x
24 prcom ⊢ m y = y m
25 24 eleq1i ⊢ m y ∈ Edg ⁡ G ↔ y m ∈ Edg ⁡ G
26 23 25 anbi12ci ⊢ x ≠ y ∧ m y ∈ Edg ⁡ G ↔ y m ∈ Edg ⁡ G ∧ ¬ y = x
27 26 anbi2i ⊢ x m ∈ Edg ⁡ G ∧ x ≠ y ∧ m y ∈ Edg ⁡ G ↔ x m ∈ Edg ⁡ G ∧ y m ∈ Edg ⁡ G ∧ ¬ y = x
28 22 27 bitri ⊢ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ↔ x m ∈ Edg ⁡ G ∧ y m ∈ Edg ⁡ G ∧ ¬ y = x
29 28 anbi1i ⊢ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ∧ z = ⟨“ xmy ”⟩ ↔ x m ∈ Edg ⁡ G ∧ y m ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xmy ”⟩
30 20 21 29 3bitri ⊢ z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ↔ x m ∈ Edg ⁡ G ∧ y m ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xmy ”⟩
31 preq2 ⊢ m = N → x m = x N
32 31 eleq1d ⊢ m = N → x m ∈ Edg ⁡ G ↔ x N ∈ Edg ⁡ G
33 preq2 ⊢ m = N → y m = y N
34 33 eleq1d ⊢ m = N → y m ∈ Edg ⁡ G ↔ y N ∈ Edg ⁡ G
35 34 anbi1d ⊢ m = N → y m ∈ Edg ⁡ G ∧ ¬ y = x ↔ y N ∈ Edg ⁡ G ∧ ¬ y = x
36 32 35 anbi12d ⊢ m = N → x m ∈ Edg ⁡ G ∧ y m ∈ Edg ⁡ G ∧ ¬ y = x ↔ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x
37 s3eq2 ⊢ m = N → ⟨“ xmy ”⟩ = ⟨“ xNy ”⟩
38 37 eqeq2d ⊢ m = N → z = ⟨“ xmy ”⟩ ↔ z = ⟨“ xNy ”⟩
39 36 38 anbi12d ⊢ m = N → x m ∈ Edg ⁡ G ∧ y m ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xmy ”⟩ ↔ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xNy ”⟩
40 30 39 syl5bb ⊢ m = N → z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ↔ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xNy ”⟩
41 40 adantl ⊢ G ∈ FinUSGraph ∧ N ∈ V ∧ x ∈ V ∧ y ∈ V ∧ z ⁡ 1 = N ∧ m = N → z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ↔ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xNy ”⟩
42 fveq1 ⊢ z = ⟨“ xmy ”⟩ → z ⁡ 1 = ⟨“ xmy ”⟩ ⁡ 1
43 s3fv1 ⊢ m ∈ V → ⟨“ xmy ”⟩ ⁡ 1 = m
44 43 elv ⊢ ⟨“ xmy ”⟩ ⁡ 1 = m
45 42 44 eqtrdi ⊢ z = ⟨“ xmy ”⟩ → z ⁡ 1 = m
46 45 eqeq1d ⊢ z = ⟨“ xmy ”⟩ → z ⁡ 1 = N ↔ m = N
47 46 biimpd ⊢ z = ⟨“ xmy ”⟩ → z ⁡ 1 = N → m = N
48 47 adantr ⊢ z = ⟨“ xmy ”⟩ ∧ x ≠ y → z ⁡ 1 = N → m = N
49 48 adantr ⊢ z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G → z ⁡ 1 = N → m = N
50 49 com12 ⊢ z ⁡ 1 = N → z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G → m = N
51 50 ad2antll ⊢ G ∈ FinUSGraph ∧ N ∈ V ∧ x ∈ V ∧ y ∈ V ∧ z ⁡ 1 = N → z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G → m = N
52 51 imp ⊢ G ∈ FinUSGraph ∧ N ∈ V ∧ x ∈ V ∧ y ∈ V ∧ z ⁡ 1 = N ∧ z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G → m = N
53 19 41 52 rspcebdv ⊢ G ∈ FinUSGraph ∧ N ∈ V ∧ x ∈ V ∧ y ∈ V ∧ z ⁡ 1 = N → ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ↔ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xNy ”⟩
54 53 pm5.32da ⊢ G ∈ FinUSGraph ∧ N ∈ V → x ∈ V ∧ y ∈ V ∧ z ⁡ 1 = N ∧ ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ↔ x ∈ V ∧ y ∈ V ∧ z ⁡ 1 = N ∧ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xNy ”⟩
55 an32 ⊢ x ∈ V ∧ y ∈ V ∧ ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ∧ z ⁡ 1 = N ↔ x ∈ V ∧ y ∈ V ∧ z ⁡ 1 = N ∧ ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G
56 55 a1i ⊢ G ∈ FinUSGraph ∧ N ∈ V → x ∈ V ∧ y ∈ V ∧ ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ∧ z ⁡ 1 = N ↔ x ∈ V ∧ y ∈ V ∧ z ⁡ 1 = N ∧ ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G
57 usgrumgr ⊢ G ∈ USGraph → G ∈ UMGraph
58 1 8 umgrpredgv ⊢ G ∈ UMGraph ∧ x N ∈ Edg ⁡ G → x ∈ V ∧ N ∈ V
59 58 simpld ⊢ G ∈ UMGraph ∧ x N ∈ Edg ⁡ G → x ∈ V
60 59 ex ⊢ G ∈ UMGraph → x N ∈ Edg ⁡ G → x ∈ V
61 1 8 umgrpredgv ⊢ G ∈ UMGraph ∧ y N ∈ Edg ⁡ G → y ∈ V ∧ N ∈ V
62 61 simpld ⊢ G ∈ UMGraph ∧ y N ∈ Edg ⁡ G → y ∈ V
63 62 expcom ⊢ y N ∈ Edg ⁡ G → G ∈ UMGraph → y ∈ V
64 63 adantr ⊢ y N ∈ Edg ⁡ G ∧ ¬ y = x → G ∈ UMGraph → y ∈ V
65 64 com12 ⊢ G ∈ UMGraph → y N ∈ Edg ⁡ G ∧ ¬ y = x → y ∈ V
66 60 65 anim12d ⊢ G ∈ UMGraph → x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x → x ∈ V ∧ y ∈ V
67 6 57 66 3syl ⊢ G ∈ FinUSGraph → x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x → x ∈ V ∧ y ∈ V
68 67 adantr ⊢ G ∈ FinUSGraph ∧ N ∈ V → x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x → x ∈ V ∧ y ∈ V
69 68 com12 ⊢ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x → G ∈ FinUSGraph ∧ N ∈ V → x ∈ V ∧ y ∈ V
70 69 adantr ⊢ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xNy ”⟩ → G ∈ FinUSGraph ∧ N ∈ V → x ∈ V ∧ y ∈ V
71 70 impcom ⊢ G ∈ FinUSGraph ∧ N ∈ V ∧ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xNy ”⟩ → x ∈ V ∧ y ∈ V
72 fveq1 ⊢ z = ⟨“ xNy ”⟩ → z ⁡ 1 = ⟨“ xNy ”⟩ ⁡ 1
73 72 adantl ⊢ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xNy ”⟩ → z ⁡ 1 = ⟨“ xNy ”⟩ ⁡ 1
74 s3fv1 ⊢ N ∈ V → ⟨“ xNy ”⟩ ⁡ 1 = N
75 74 adantl ⊢ G ∈ FinUSGraph ∧ N ∈ V → ⟨“ xNy ”⟩ ⁡ 1 = N
76 73 75 sylan9eqr ⊢ G ∈ FinUSGraph ∧ N ∈ V ∧ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xNy ”⟩ → z ⁡ 1 = N
77 71 76 jca ⊢ G ∈ FinUSGraph ∧ N ∈ V ∧ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xNy ”⟩ → x ∈ V ∧ y ∈ V ∧ z ⁡ 1 = N
78 77 ex ⊢ G ∈ FinUSGraph ∧ N ∈ V → x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xNy ”⟩ → x ∈ V ∧ y ∈ V ∧ z ⁡ 1 = N
79 78 pm4.71rd ⊢ G ∈ FinUSGraph ∧ N ∈ V → x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xNy ”⟩ ↔ x ∈ V ∧ y ∈ V ∧ z ⁡ 1 = N ∧ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xNy ”⟩
80 54 56 79 3bitr4d ⊢ G ∈ FinUSGraph ∧ N ∈ V → x ∈ V ∧ y ∈ V ∧ ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ∧ z ⁡ 1 = N ↔ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z = ⟨“ xNy ”⟩
81 8 nbusgreledg ⊢ G ∈ USGraph → x ∈ G NeighbVtx N ↔ x N ∈ Edg ⁡ G
82 6 81 syl ⊢ G ∈ FinUSGraph → x ∈ G NeighbVtx N ↔ x N ∈ Edg ⁡ G
83 82 adantr ⊢ G ∈ FinUSGraph ∧ N ∈ V → x ∈ G NeighbVtx N ↔ x N ∈ Edg ⁡ G
84 eldif ⊢ y ∈ G NeighbVtx N ∖ x ↔ y ∈ G NeighbVtx N ∧ ¬ y ∈ x
85 8 nbusgreledg ⊢ G ∈ USGraph → y ∈ G NeighbVtx N ↔ y N ∈ Edg ⁡ G
86 6 85 syl ⊢ G ∈ FinUSGraph → y ∈ G NeighbVtx N ↔ y N ∈ Edg ⁡ G
87 86 adantr ⊢ G ∈ FinUSGraph ∧ N ∈ V → y ∈ G NeighbVtx N ↔ y N ∈ Edg ⁡ G
88 velsn ⊢ y ∈ x ↔ y = x
89 88 a1i ⊢ G ∈ FinUSGraph ∧ N ∈ V → y ∈ x ↔ y = x
90 89 notbid ⊢ G ∈ FinUSGraph ∧ N ∈ V → ¬ y ∈ x ↔ ¬ y = x
91 87 90 anbi12d ⊢ G ∈ FinUSGraph ∧ N ∈ V → y ∈ G NeighbVtx N ∧ ¬ y ∈ x ↔ y N ∈ Edg ⁡ G ∧ ¬ y = x
92 84 91 syl5bb ⊢ G ∈ FinUSGraph ∧ N ∈ V → y ∈ G NeighbVtx N ∖ x ↔ y N ∈ Edg ⁡ G ∧ ¬ y = x
93 83 92 anbi12d ⊢ G ∈ FinUSGraph ∧ N ∈ V → x ∈ G NeighbVtx N ∧ y ∈ G NeighbVtx N ∖ x ↔ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x
94 93 anbi1d ⊢ G ∈ FinUSGraph ∧ N ∈ V → x ∈ G NeighbVtx N ∧ y ∈ G NeighbVtx N ∖ x ∧ z ∈ ⟨“ xNy ”⟩ ↔ x N ∈ Edg ⁡ G ∧ y N ∈ Edg ⁡ G ∧ ¬ y = x ∧ z ∈ ⟨“ xNy ”⟩
95 18 80 94 3bitr4d ⊢ G ∈ FinUSGraph ∧ N ∈ V → x ∈ V ∧ y ∈ V ∧ ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ∧ z ⁡ 1 = N ↔ x ∈ G NeighbVtx N ∧ y ∈ G NeighbVtx N ∖ x ∧ z ∈ ⟨“ xNy ”⟩
96 95 2exbidv ⊢ G ∈ FinUSGraph ∧ N ∈ V → ∃ x ∃ y x ∈ V ∧ y ∈ V ∧ ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ∧ z ⁡ 1 = N ↔ ∃ x ∃ y x ∈ G NeighbVtx N ∧ y ∈ G NeighbVtx N ∖ x ∧ z ∈ ⟨“ xNy ”⟩
97 14 96 bitr3id ⊢ G ∈ FinUSGraph ∧ N ∈ V → ∃ x ∃ y x ∈ V ∧ y ∈ V ∧ ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ∧ z ⁡ 1 = N ↔ ∃ x ∃ y x ∈ G NeighbVtx N ∧ y ∈ G NeighbVtx N ∖ x ∧ z ∈ ⟨“ xNy ”⟩
98 r2ex ⊢ ∃ x ∈ V ∃ y ∈ V ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ↔ ∃ x ∃ y x ∈ V ∧ y ∈ V ∧ ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G
99 98 anbi1i ⊢ ∃ x ∈ V ∃ y ∈ V ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ∧ z ⁡ 1 = N ↔ ∃ x ∃ y x ∈ V ∧ y ∈ V ∧ ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ∧ z ⁡ 1 = N
100 r2ex ⊢ ∃ x ∈ G NeighbVtx N ∃ y ∈ G NeighbVtx N ∖ x z ∈ ⟨“ xNy ”⟩ ↔ ∃ x ∃ y x ∈ G NeighbVtx N ∧ y ∈ G NeighbVtx N ∖ x ∧ z ∈ ⟨“ xNy ”⟩
101 97 99 100 3bitr4g ⊢ G ∈ FinUSGraph ∧ N ∈ V → ∃ x ∈ V ∃ y ∈ V ∃ m ∈ V z = ⟨“ xmy ”⟩ ∧ x ≠ y ∧ x m ∈ Edg ⁡ G ∧ m y ∈ Edg ⁡ G ∧ z ⁡ 1 = N ↔ ∃ x ∈ G NeighbVtx N ∃ y ∈ G NeighbVtx N ∖ x z ∈ ⟨“ xNy ”⟩
102 vex ⊢ z ∈ V
103 eleq1w ⊢ p = z → p ∈ ⟨“ xNy ”⟩ ↔ z ∈ ⟨“ xNy ”⟩
104 103 2rexbidv ⊢ p = z → ∃ x ∈ G NeighbVtx N ∃ y ∈ G NeighbVtx N ∖ x p ∈ ⟨“ xNy ”⟩ ↔ ∃ x ∈ G NeighbVtx N ∃ y ∈ G NeighbVtx N ∖ x z ∈ ⟨“ xNy ”⟩
105 102 104 elab ⊢ z ∈ p | ∃ x ∈ G NeighbVtx N ∃ y ∈ G NeighbVtx N ∖ x p ∈ ⟨“ xNy ”⟩ ↔ ∃ x ∈ G NeighbVtx N ∃ y ∈ G NeighbVtx N ∖ x z ∈ ⟨“ xNy ”⟩
106 105 bicomi ⊢ ∃ x ∈ G NeighbVtx N ∃ y ∈ G NeighbVtx N ∖ x z ∈ ⟨“ xNy ”⟩ ↔ z ∈ p | ∃ x ∈ G NeighbVtx N ∃ y ∈ G NeighbVtx N ∖ x p ∈ ⟨“ xNy ”⟩
107 106 a1i ⊢ G ∈ FinUSGraph ∧ N ∈ V → ∃ x ∈ G NeighbVtx N ∃ y ∈ G NeighbVtx N ∖ x z ∈ ⟨“ xNy ”⟩ ↔ z ∈ p | ∃ x ∈ G NeighbVtx N ∃ y ∈ G NeighbVtx N ∖ x p ∈ ⟨“ xNy ”⟩
108 13 101 107 3bitrd ⊢ G ∈ FinUSGraph ∧ N ∈ V → z ∈ 2 WSPathsN G ∧ z ⁡ 1 = N ↔ z ∈ p | ∃ x ∈ G NeighbVtx N ∃ y ∈ G NeighbVtx N ∖ x p ∈ ⟨“ xNy ”⟩
109 4 108 bitrd ⊢ G ∈ FinUSGraph ∧ N ∈ V → z ∈ M ⁡ N ↔ z ∈ p | ∃ x ∈ G NeighbVtx N ∃ y ∈ G NeighbVtx N ∖ x p ∈ ⟨“ xNy ”⟩
110 109 eqrdv ⊢ G ∈ FinUSGraph ∧ N ∈ V → M ⁡ N = p | ∃ x ∈ G NeighbVtx N ∃ y ∈ G NeighbVtx N ∖ x p ∈ ⟨“ xNy ”⟩
111 dfiunv2 ⊢ ⋃ x ∈ G NeighbVtx N ⋃ y ∈ G NeighbVtx N ∖ x ⟨“ xNy ”⟩ = p | ∃ x ∈ G NeighbVtx N ∃ y ∈ G NeighbVtx N ∖ x p ∈ ⟨“ xNy ”⟩
112 110 111 eqtr4di ⊢ G ∈ FinUSGraph ∧ N ∈ V → M ⁡ N = ⋃ x ∈ G NeighbVtx N ⋃ y ∈ G NeighbVtx N ∖ x ⟨“ xNy ”⟩