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 e. V |-> { w e. ( 2 WSPathsN G ) | ( w ` 1 ) = a } )
Assertion fusgr2wsp2nb 
|- ( ( G e. FinUSGraph /\ N e. V ) -> ( M ` N ) = U_ x e. ( G NeighbVtx N ) U_ y e. ( ( G NeighbVtx N ) \ { x } ) { <" x N y "> } )

Proof

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