This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nb3grprlem2

Description: Lemma 2 for nb3grpr . (Contributed by Alexander van der Vekens, 17-Oct-2017) (Revised by AV, 28-Oct-2020) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypotheses nb3grpr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
nb3grpr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
nb3grpr.g ⊢ ( 𝜑 → 𝐺 ∈ USGraph )
nb3grpr.t ⊢ ( 𝜑 → 𝑉 = { 𝐴 , 𝐵 , 𝐶 } )
nb3grpr.s ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) )
nb3grpr.n ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) )
Assertion nb3grprlem2 ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ↔ ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑣 , 𝑤 } ) )

Proof

Step Hyp Ref Expression
1 nb3grpr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 nb3grpr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 nb3grpr.g ⊢ ( 𝜑 → 𝐺 ∈ USGraph )
4 nb3grpr.t ⊢ ( 𝜑 → 𝑉 = { 𝐴 , 𝐵 , 𝐶 } )
5 nb3grpr.s ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) )
6 nb3grpr.n ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) )
7 sneq ⊢ ( 𝑣 = 𝐴 → { 𝑣 } = { 𝐴 } )
8 7 difeq2d ⊢ ( 𝑣 = 𝐴 → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑣 } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) )
9 preq1 ⊢ ( 𝑣 = 𝐴 → { 𝑣 , 𝑤 } = { 𝐴 , 𝑤 } )
10 9 eqeq2d ⊢ ( 𝑣 = 𝐴 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝑣 , 𝑤 } ↔ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ) )
11 8 10 rexeqbidv ⊢ ( 𝑣 = 𝐴 → ( ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑣 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑣 , 𝑤 } ↔ ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ) )
12 sneq ⊢ ( 𝑣 = 𝐵 → { 𝑣 } = { 𝐵 } )
13 12 difeq2d ⊢ ( 𝑣 = 𝐵 → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑣 } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) )
14 preq1 ⊢ ( 𝑣 = 𝐵 → { 𝑣 , 𝑤 } = { 𝐵 , 𝑤 } )
15 14 eqeq2d ⊢ ( 𝑣 = 𝐵 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝑣 , 𝑤 } ↔ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ) )
16 13 15 rexeqbidv ⊢ ( 𝑣 = 𝐵 → ( ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑣 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑣 , 𝑤 } ↔ ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ) )
17 sneq ⊢ ( 𝑣 = 𝐶 → { 𝑣 } = { 𝐶 } )
18 17 difeq2d ⊢ ( 𝑣 = 𝐶 → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑣 } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) )
19 preq1 ⊢ ( 𝑣 = 𝐶 → { 𝑣 , 𝑤 } = { 𝐶 , 𝑤 } )
20 19 eqeq2d ⊢ ( 𝑣 = 𝐶 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝑣 , 𝑤 } ↔ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ) )
21 18 20 rexeqbidv ⊢ ( 𝑣 = 𝐶 → ( ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑣 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑣 , 𝑤 } ↔ ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ) )
22 11 16 21 rextpg ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ∃ 𝑣 ∈ { 𝐴 , 𝐵 , 𝐶 } ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑣 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑣 , 𝑤 } ↔ ( ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ∨ ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ∨ ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ) ) )
23 5 22 syl ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ { 𝐴 , 𝐵 , 𝐶 } ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑣 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑣 , 𝑤 } ↔ ( ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ∨ ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ∨ ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ) ) )
24 4 3 jca ⊢ ( 𝜑 → ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) )
25 simpl ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → 𝑉 = { 𝐴 , 𝐵 , 𝐶 } )
26 difeq1 ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( 𝑉 ∖ { 𝑣 } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑣 } ) )
27 26 adantr ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( 𝑉 ∖ { 𝑣 } ) = ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑣 } ) )
28 27 rexeqdv ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( ∃ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑣 , 𝑤 } ↔ ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑣 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑣 , 𝑤 } ) )
29 25 28 rexeqbidv ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ∧ 𝐺 ∈ USGraph ) → ( ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑣 , 𝑤 } ↔ ∃ 𝑣 ∈ { 𝐴 , 𝐵 , 𝐶 } ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑣 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑣 , 𝑤 } ) )
30 24 29 syl ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑣 , 𝑤 } ↔ ∃ 𝑣 ∈ { 𝐴 , 𝐵 , 𝐶 } ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝑣 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑣 , 𝑤 } ) )
31 preq2 ⊢ ( 𝑤 = 𝐵 → { 𝐴 , 𝑤 } = { 𝐴 , 𝐵 } )
32 31 eqeq2d ⊢ ( 𝑤 = 𝐵 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ↔ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } ) )
33 preq2 ⊢ ( 𝑤 = 𝐶 → { 𝐴 , 𝑤 } = { 𝐴 , 𝐶 } )
34 33 eqeq2d ⊢ ( 𝑤 = 𝐶 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ↔ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } ) )
35 32 34 rexprg ⊢ ( ( 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ∃ 𝑤 ∈ { 𝐵 , 𝐶 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } ) ) )
36 35 3adant1 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ∃ 𝑤 ∈ { 𝐵 , 𝐶 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } ) ) )
37 preq2 ⊢ ( 𝑤 = 𝐶 → { 𝐵 , 𝑤 } = { 𝐵 , 𝐶 } )
38 37 eqeq2d ⊢ ( 𝑤 = 𝐶 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ↔ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ) )
39 preq2 ⊢ ( 𝑤 = 𝐴 → { 𝐵 , 𝑤 } = { 𝐵 , 𝐴 } )
40 39 eqeq2d ⊢ ( 𝑤 = 𝐴 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ↔ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ) )
41 38 40 rexprg ⊢ ( ( 𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ) → ( ∃ 𝑤 ∈ { 𝐶 , 𝐴 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ) ) )
42 41 ancoms ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍 ) → ( ∃ 𝑤 ∈ { 𝐶 , 𝐴 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ) ) )
43 42 3adant2 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ∃ 𝑤 ∈ { 𝐶 , 𝐴 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ) ) )
44 preq2 ⊢ ( 𝑤 = 𝐴 → { 𝐶 , 𝑤 } = { 𝐶 , 𝐴 } )
45 44 eqeq2d ⊢ ( 𝑤 = 𝐴 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ↔ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } ) )
46 preq2 ⊢ ( 𝑤 = 𝐵 → { 𝐶 , 𝑤 } = { 𝐶 , 𝐵 } )
47 46 eqeq2d ⊢ ( 𝑤 = 𝐵 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ↔ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ) )
48 45 47 rexprg ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ∃ 𝑤 ∈ { 𝐴 , 𝐵 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ) ) )
49 48 3adant3 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ∃ 𝑤 ∈ { 𝐴 , 𝐵 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ) ) )
50 36 43 49 3orbi123d ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ( ∃ 𝑤 ∈ { 𝐵 , 𝐶 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ∨ ∃ 𝑤 ∈ { 𝐶 , 𝐴 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ∨ ∃ 𝑤 ∈ { 𝐴 , 𝐵 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ) ↔ ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } ) ∨ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ) ∨ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ) ) ) )
51 5 50 syl ⊢ ( 𝜑 → ( ( ∃ 𝑤 ∈ { 𝐵 , 𝐶 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ∨ ∃ 𝑤 ∈ { 𝐶 , 𝐴 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ∨ ∃ 𝑤 ∈ { 𝐴 , 𝐵 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ) ↔ ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } ) ∨ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ) ∨ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ) ) ) )
52 tprot ⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐶 , 𝐴 }
53 52 a1i ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐶 , 𝐴 } )
54 53 difeq1d ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) = ( { 𝐵 , 𝐶 , 𝐴 } ∖ { 𝐴 } ) )
55 necom ⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
56 necom ⊢ ( 𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴 )
57 diftpsn3 ⊢ ( ( 𝐵 ≠ 𝐴 ∧ 𝐶 ≠ 𝐴 ) → ( { 𝐵 , 𝐶 , 𝐴 } ∖ { 𝐴 } ) = { 𝐵 , 𝐶 } )
58 55 56 57 syl2anb ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) → ( { 𝐵 , 𝐶 , 𝐴 } ∖ { 𝐴 } ) = { 𝐵 , 𝐶 } )
59 58 3adant3 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐵 , 𝐶 , 𝐴 } ∖ { 𝐴 } ) = { 𝐵 , 𝐶 } )
60 54 59 eqtrd ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) = { 𝐵 , 𝐶 } )
61 60 rexeqdv ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ↔ ∃ 𝑤 ∈ { 𝐵 , 𝐶 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ) )
62 tprot ⊢ { 𝐶 , 𝐴 , 𝐵 } = { 𝐴 , 𝐵 , 𝐶 }
63 62 eqcomi ⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐶 , 𝐴 , 𝐵 }
64 63 a1i ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → { 𝐴 , 𝐵 , 𝐶 } = { 𝐶 , 𝐴 , 𝐵 } )
65 64 difeq1d ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) = ( { 𝐶 , 𝐴 , 𝐵 } ∖ { 𝐵 } ) )
66 necom ⊢ ( 𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵 )
67 66 anbi1i ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ) ↔ ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) )
68 67 biimpi ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) )
69 68 ancoms ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) )
70 diftpsn3 ⊢ ( ( 𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐶 , 𝐴 , 𝐵 } ∖ { 𝐵 } ) = { 𝐶 , 𝐴 } )
71 69 70 syl ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐶 , 𝐴 , 𝐵 } ∖ { 𝐵 } ) = { 𝐶 , 𝐴 } )
72 71 3adant2 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐶 , 𝐴 , 𝐵 } ∖ { 𝐵 } ) = { 𝐶 , 𝐴 } )
73 65 72 eqtrd ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) = { 𝐶 , 𝐴 } )
74 73 rexeqdv ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ↔ ∃ 𝑤 ∈ { 𝐶 , 𝐴 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ) )
75 diftpsn3 ⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) = { 𝐴 , 𝐵 } )
76 75 3adant1 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) = { 𝐴 , 𝐵 } )
77 76 rexeqdv ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ↔ ∃ 𝑤 ∈ { 𝐴 , 𝐵 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ) )
78 61 74 77 3orbi123d ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ( ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ∨ ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ∨ ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ) ↔ ( ∃ 𝑤 ∈ { 𝐵 , 𝐶 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ∨ ∃ 𝑤 ∈ { 𝐶 , 𝐴 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ∨ ∃ 𝑤 ∈ { 𝐴 , 𝐵 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ) ) )
79 6 78 syl ⊢ ( 𝜑 → ( ( ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ∨ ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ∨ ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ) ↔ ( ∃ 𝑤 ∈ { 𝐵 , 𝐶 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ∨ ∃ 𝑤 ∈ { 𝐶 , 𝐴 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ∨ ∃ 𝑤 ∈ { 𝐴 , 𝐵 } ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ) ) )
80 prcom ⊢ { 𝐶 , 𝐵 } = { 𝐵 , 𝐶 }
81 80 eqeq2i ⊢ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ↔ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } )
82 81 orbi2i ⊢ ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ) ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ) )
83 oridm ⊢ ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ) ↔ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } )
84 82 83 bitr2i ⊢ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ) )
85 84 a1i ⊢ ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ) ) )
86 nbgrnself2 ⊢ 𝐴 ∉ ( 𝐺 NeighbVtx 𝐴 )
87 df-nel ⊢ ( 𝐴 ∉ ( 𝐺 NeighbVtx 𝐴 ) ↔ ¬ 𝐴 ∈ ( 𝐺 NeighbVtx 𝐴 ) )
88 prid2g ⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ { 𝐵 , 𝐴 } )
89 88 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → 𝐴 ∈ { 𝐵 , 𝐴 } )
90 eleq2 ⊢ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } → ( 𝐴 ∈ ( 𝐺 NeighbVtx 𝐴 ) ↔ 𝐴 ∈ { 𝐵 , 𝐴 } ) )
91 89 90 syl5ibrcom ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } → 𝐴 ∈ ( 𝐺 NeighbVtx 𝐴 ) ) )
92 91 con3rr3 ⊢ ( ¬ 𝐴 ∈ ( 𝐺 NeighbVtx 𝐴 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ) )
93 87 92 sylbi ⊢ ( 𝐴 ∉ ( 𝐺 NeighbVtx 𝐴 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ) )
94 86 5 93 mpsyl ⊢ ( 𝜑 → ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } )
95 biorf ⊢ ( ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ) ) )
96 orcom ⊢ ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ) ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ) )
97 95 96 bitrdi ⊢ ( ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ) ) )
98 94 97 syl ⊢ ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ) ) )
99 prid2g ⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ { 𝐶 , 𝐴 } )
100 99 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → 𝐴 ∈ { 𝐶 , 𝐴 } )
101 eleq2 ⊢ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } → ( 𝐴 ∈ ( 𝐺 NeighbVtx 𝐴 ) ↔ 𝐴 ∈ { 𝐶 , 𝐴 } ) )
102 100 101 syl5ibrcom ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } → 𝐴 ∈ ( 𝐺 NeighbVtx 𝐴 ) ) )
103 102 con3rr3 ⊢ ( ¬ 𝐴 ∈ ( 𝐺 NeighbVtx 𝐴 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } ) )
104 87 103 sylbi ⊢ ( 𝐴 ∉ ( 𝐺 NeighbVtx 𝐴 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } ) )
105 86 5 104 mpsyl ⊢ ( 𝜑 → ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } )
106 biorf ⊢ ( ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ) ) )
107 105 106 syl ⊢ ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ↔ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ) ) )
108 98 107 orbi12d ⊢ ( 𝜑 → ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ) ↔ ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ) ∨ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ) ) ) )
109 prid1g ⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ { 𝐴 , 𝐵 } )
110 109 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → 𝐴 ∈ { 𝐴 , 𝐵 } )
111 eleq2 ⊢ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } → ( 𝐴 ∈ ( 𝐺 NeighbVtx 𝐴 ) ↔ 𝐴 ∈ { 𝐴 , 𝐵 } ) )
112 110 111 syl5ibrcom ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } → 𝐴 ∈ ( 𝐺 NeighbVtx 𝐴 ) ) )
113 112 con3dimp ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ¬ 𝐴 ∈ ( 𝐺 NeighbVtx 𝐴 ) ) → ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } )
114 prid1g ⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ { 𝐴 , 𝐶 } )
115 114 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → 𝐴 ∈ { 𝐴 , 𝐶 } )
116 eleq2 ⊢ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } → ( 𝐴 ∈ ( 𝐺 NeighbVtx 𝐴 ) ↔ 𝐴 ∈ { 𝐴 , 𝐶 } ) )
117 115 116 syl5ibrcom ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } → 𝐴 ∈ ( 𝐺 NeighbVtx 𝐴 ) ) )
118 117 con3dimp ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ¬ 𝐴 ∈ ( 𝐺 NeighbVtx 𝐴 ) ) → ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } )
119 113 118 jca ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ∧ ¬ 𝐴 ∈ ( 𝐺 NeighbVtx 𝐴 ) ) → ( ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } ∧ ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } ) )
120 119 expcom ⊢ ( ¬ 𝐴 ∈ ( 𝐺 NeighbVtx 𝐴 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } ∧ ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } ) ) )
121 87 120 sylbi ⊢ ( 𝐴 ∉ ( 𝐺 NeighbVtx 𝐴 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } ∧ ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } ) ) )
122 86 5 121 mpsyl ⊢ ( 𝜑 → ( ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } ∧ ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } ) )
123 ioran ⊢ ( ¬ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } ) ↔ ( ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } ∧ ¬ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } ) )
124 122 123 sylibr ⊢ ( 𝜑 → ¬ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } ) )
125 124 3bior1fd ⊢ ( 𝜑 → ( ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ) ∨ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ) ) ↔ ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } ) ∨ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ) ∨ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ) ) ) )
126 85 108 125 3bitrd ⊢ ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ↔ ( ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐵 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝐶 } ) ∨ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐴 } ) ∨ ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐴 } ∨ ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝐵 } ) ) ) )
127 51 79 126 3bitr4rd ⊢ ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ↔ ( ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐴 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐴 , 𝑤 } ∨ ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐵 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝑤 } ∨ ∃ 𝑤 ∈ ( { 𝐴 , 𝐵 , 𝐶 } ∖ { 𝐶 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝐶 , 𝑤 } ) ) )
128 23 30 127 3bitr4rd ⊢ ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ↔ ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) ( 𝐺 NeighbVtx 𝐴 ) = { 𝑣 , 𝑤 } ) )