Metamath Proof Explorer

Theorem nbgr2vtx1edg

Description: If a graph has two vertices, and there is an edge between the vertices, then each vertex is the neighbor of the other vertex. (Contributed by AV, 2-Nov-2020) (Revised by AV, 25-Mar-2021) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypotheses nbgr2vtx1edg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
nbgr2vtx1edg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion nbgr2vtx1edg ( ( ( ♯ ‘ 𝑉 ) = 2 ∧ 𝑉 ∈ 𝐸 ) → ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) )

Proof

Step Hyp Ref Expression
1 nbgr2vtx1edg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 nbgr2vtx1edg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 fvexi ⊢ 𝑉 ∈ V
4 hash2prb ⊢ ( 𝑉 ∈ V → ( ( ♯ ‘ 𝑉 ) = 2 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) )
5 3 4 ax-mp ⊢ ( ( ♯ ‘ 𝑉 ) = 2 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) )
6 simpll ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) )
7 6 ancomd ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → ( 𝑏 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉 ) )
8 simpl ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) → 𝑎 ≠ 𝑏 )
9 8 necomd ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) → 𝑏 ≠ 𝑎 )
10 9 ad2antlr ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → 𝑏 ≠ 𝑎 )
11 id ⊢ ( { 𝑎 , 𝑏 } ∈ 𝐸 → { 𝑎 , 𝑏 } ∈ 𝐸 )
12 sseq2 ⊢ ( 𝑒 = { 𝑎 , 𝑏 } → ( { 𝑎 , 𝑏 } ⊆ 𝑒 ↔ { 𝑎 , 𝑏 } ⊆ { 𝑎 , 𝑏 } ) )
13 12 adantl ⊢ ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ 𝑒 = { 𝑎 , 𝑏 } ) → ( { 𝑎 , 𝑏 } ⊆ 𝑒 ↔ { 𝑎 , 𝑏 } ⊆ { 𝑎 , 𝑏 } ) )
14 ssidd ⊢ ( { 𝑎 , 𝑏 } ∈ 𝐸 → { 𝑎 , 𝑏 } ⊆ { 𝑎 , 𝑏 } )
15 11 13 14 rspcedvd ⊢ ( { 𝑎 , 𝑏 } ∈ 𝐸 → ∃ 𝑒 ∈ 𝐸 { 𝑎 , 𝑏 } ⊆ 𝑒 )
16 15 adantl ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → ∃ 𝑒 ∈ 𝐸 { 𝑎 , 𝑏 } ⊆ 𝑒 )
17 1 2 nbgrel ⊢ ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ↔ ( ( 𝑏 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ≠ 𝑎 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑎 , 𝑏 } ⊆ 𝑒 ) )
18 7 10 16 17 syl3anbrc ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) )
19 8 ad2antlr ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → 𝑎 ≠ 𝑏 )
20 sseq2 ⊢ ( 𝑒 = { 𝑎 , 𝑏 } → ( { 𝑏 , 𝑎 } ⊆ 𝑒 ↔ { 𝑏 , 𝑎 } ⊆ { 𝑎 , 𝑏 } ) )
21 20 adantl ⊢ ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ 𝑒 = { 𝑎 , 𝑏 } ) → ( { 𝑏 , 𝑎 } ⊆ 𝑒 ↔ { 𝑏 , 𝑎 } ⊆ { 𝑎 , 𝑏 } ) )
22 prcom ⊢ { 𝑏 , 𝑎 } = { 𝑎 , 𝑏 }
23 22 eqimssi ⊢ { 𝑏 , 𝑎 } ⊆ { 𝑎 , 𝑏 }
24 23 a1i ⊢ ( { 𝑎 , 𝑏 } ∈ 𝐸 → { 𝑏 , 𝑎 } ⊆ { 𝑎 , 𝑏 } )
25 11 21 24 rspcedvd ⊢ ( { 𝑎 , 𝑏 } ∈ 𝐸 → ∃ 𝑒 ∈ 𝐸 { 𝑏 , 𝑎 } ⊆ 𝑒 )
26 25 adantl ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → ∃ 𝑒 ∈ 𝐸 { 𝑏 , 𝑎 } ⊆ 𝑒 )
27 1 2 nbgrel ⊢ ( 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ↔ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑎 ≠ 𝑏 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑏 , 𝑎 } ⊆ 𝑒 ) )
28 6 19 26 27 syl3anbrc ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) )
29 difprsn1 ⊢ ( 𝑎 ≠ 𝑏 → ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) = { 𝑏 } )
30 29 raleqdv ⊢ ( 𝑎 ≠ 𝑏 → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ↔ ∀ 𝑛 ∈ { 𝑏 } 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
31 vex ⊢ 𝑏 ∈ V
32 eleq1 ⊢ ( 𝑛 = 𝑏 → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ↔ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
33 31 32 ralsn ⊢ ( ∀ 𝑛 ∈ { 𝑏 } 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ↔ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) )
34 30 33 bitrdi ⊢ ( 𝑎 ≠ 𝑏 → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ↔ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
35 difprsn2 ⊢ ( 𝑎 ≠ 𝑏 → ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) = { 𝑎 } )
36 35 raleqdv ⊢ ( 𝑎 ≠ 𝑏 → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ↔ ∀ 𝑛 ∈ { 𝑎 } 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) )
37 vex ⊢ 𝑎 ∈ V
38 eleq1 ⊢ ( 𝑛 = 𝑎 → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ↔ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) )
39 37 38 ralsn ⊢ ( ∀ 𝑛 ∈ { 𝑎 } 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ↔ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) )
40 36 39 bitrdi ⊢ ( 𝑎 ≠ 𝑏 → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ↔ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) )
41 34 40 anbi12d ⊢ ( 𝑎 ≠ 𝑏 → ( ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ↔ ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ) )
42 41 adantr ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ↔ ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ) )
43 42 ad2antlr ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → ( ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ↔ ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ) )
44 18 28 43 mpbir2and ⊢ ( ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) )
45 44 ex ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ) )
46 eleq1 ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → ( 𝑉 ∈ 𝐸 ↔ { 𝑎 , 𝑏 } ∈ 𝐸 ) )
47 id ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → 𝑉 = { 𝑎 , 𝑏 } )
48 difeq1 ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → ( 𝑉 ∖ { 𝑣 } ) = ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) )
49 48 raleqdv ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
50 47 49 raleqbidv ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ∀ 𝑣 ∈ { 𝑎 , 𝑏 } ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
51 sneq ⊢ ( 𝑣 = 𝑎 → { 𝑣 } = { 𝑎 } )
52 51 difeq2d ⊢ ( 𝑣 = 𝑎 → ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) = ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) )
53 oveq2 ⊢ ( 𝑣 = 𝑎 → ( 𝐺 NeighbVtx 𝑣 ) = ( 𝐺 NeighbVtx 𝑎 ) )
54 53 eleq2d ⊢ ( 𝑣 = 𝑎 → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
55 52 54 raleqbidv ⊢ ( 𝑣 = 𝑎 → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
56 sneq ⊢ ( 𝑣 = 𝑏 → { 𝑣 } = { 𝑏 } )
57 56 difeq2d ⊢ ( 𝑣 = 𝑏 → ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) = ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) )
58 oveq2 ⊢ ( 𝑣 = 𝑏 → ( 𝐺 NeighbVtx 𝑣 ) = ( 𝐺 NeighbVtx 𝑏 ) )
59 58 eleq2d ⊢ ( 𝑣 = 𝑏 → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) )
60 57 59 raleqbidv ⊢ ( 𝑣 = 𝑏 → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) )
61 37 31 55 60 ralpr ⊢ ( ∀ 𝑣 ∈ { 𝑎 , 𝑏 } ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) )
62 50 61 bitrdi ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ) )
63 46 62 imbi12d ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → ( ( 𝑉 ∈ 𝐸 → ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ↔ ( { 𝑎 , 𝑏 } ∈ 𝐸 → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ) ) )
64 63 adantl ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( ( 𝑉 ∈ 𝐸 → ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ↔ ( { 𝑎 , 𝑏 } ∈ 𝐸 → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ) ) )
65 64 adantl ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) → ( ( 𝑉 ∈ 𝐸 → ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ↔ ( { 𝑎 , 𝑏 } ∈ 𝐸 → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ) ) )
66 45 65 mpbird ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) → ( 𝑉 ∈ 𝐸 → ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
67 66 ex ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( 𝑉 ∈ 𝐸 → ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ) )
68 67 rexlimivv ⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( 𝑉 ∈ 𝐸 → ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
69 5 68 sylbi ⊢ ( ( ♯ ‘ 𝑉 ) = 2 → ( 𝑉 ∈ 𝐸 → ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
70 69 imp ⊢ ( ( ( ♯ ‘ 𝑉 ) = 2 ∧ 𝑉 ∈ 𝐸 ) → ∀ 𝑣 ∈ 𝑉 ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) )