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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
fusgreg2wsp.m ⊢ 𝑀 = ( 𝑎 ∈ 𝑉 ↦ { 𝑤 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑤 ‘ 1 ) = 𝑎 } )
Assertion fusgr2wsp2nb ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑀 ‘ 𝑁 ) = ∪ 𝑥 ∈ ( 𝐺 NeighbVtx 𝑁 ) ∪ 𝑦 ∈ ( ( 𝐺 NeighbVtx 𝑁 ) ∖ { 𝑥 } ) { ⟨“ 𝑥 𝑁 𝑦 ”⟩ } )

Proof

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