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

Metamath Proof Explorer

Theorem nbgr1vtx

Description: In a graph with one vertex, all neighborhoods are empty. (Contributed by AV, 15-Nov-2020)

Ref Expression
Assertion nbgr1vtx ( ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 1 → ( 𝐺 NeighbVtx 𝐾 ) = ∅ )

Proof

Step Hyp Ref Expression
1 fvex ⊢ ( Vtx ‘ 𝐺 ) ∈ V
2 hash1snb ⊢ ( ( Vtx ‘ 𝐺 ) ∈ V → ( ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 1 ↔ ∃ 𝑣 ( Vtx ‘ 𝐺 ) = { 𝑣 } ) )
3 1 2 ax-mp ⊢ ( ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 1 ↔ ∃ 𝑣 ( Vtx ‘ 𝐺 ) = { 𝑣 } )
4 ral0 ⊢ ∀ 𝑛 ∈ ∅ ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒
5 eleq2 ⊢ ( ( Vtx ‘ 𝐺 ) = { 𝑣 } → ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ↔ 𝐾 ∈ { 𝑣 } ) )
6 simpr ⊢ ( ( 𝐾 = 𝑣 ∧ ( Vtx ‘ 𝐺 ) = { 𝑣 } ) → ( Vtx ‘ 𝐺 ) = { 𝑣 } )
7 sneq ⊢ ( 𝐾 = 𝑣 → { 𝐾 } = { 𝑣 } )
8 7 adantr ⊢ ( ( 𝐾 = 𝑣 ∧ ( Vtx ‘ 𝐺 ) = { 𝑣 } ) → { 𝐾 } = { 𝑣 } )
9 6 8 difeq12d ⊢ ( ( 𝐾 = 𝑣 ∧ ( Vtx ‘ 𝐺 ) = { 𝑣 } ) → ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) = ( { 𝑣 } ∖ { 𝑣 } ) )
10 difid ⊢ ( { 𝑣 } ∖ { 𝑣 } ) = ∅
11 9 10 eqtrdi ⊢ ( ( 𝐾 = 𝑣 ∧ ( Vtx ‘ 𝐺 ) = { 𝑣 } ) → ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) = ∅ )
12 11 ex ⊢ ( 𝐾 = 𝑣 → ( ( Vtx ‘ 𝐺 ) = { 𝑣 } → ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) = ∅ ) )
13 elsni ⊢ ( 𝐾 ∈ { 𝑣 } → 𝐾 = 𝑣 )
14 12 13 syl11 ⊢ ( ( Vtx ‘ 𝐺 ) = { 𝑣 } → ( 𝐾 ∈ { 𝑣 } → ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) = ∅ ) )
15 5 14 sylbid ⊢ ( ( Vtx ‘ 𝐺 ) = { 𝑣 } → ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) → ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) = ∅ ) )
16 15 imp ⊢ ( ( ( Vtx ‘ 𝐺 ) = { 𝑣 } ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) = ∅ )
17 16 raleqdv ⊢ ( ( ( Vtx ‘ 𝐺 ) = { 𝑣 } ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) → ( ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 ↔ ∀ 𝑛 ∈ ∅ ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 ) )
18 4 17 mpbiri ⊢ ( ( ( Vtx ‘ 𝐺 ) = { 𝑣 } ∧ 𝐾 ∈ ( Vtx ‘ 𝐺 ) ) → ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 )
19 18 ex ⊢ ( ( Vtx ‘ 𝐺 ) = { 𝑣 } → ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) → ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 ) )
20 19 exlimiv ⊢ ( ∃ 𝑣 ( Vtx ‘ 𝐺 ) = { 𝑣 } → ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) → ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 ) )
21 3 20 sylbi ⊢ ( ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 1 → ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) → ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 ) )
22 21 impcom ⊢ ( ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 1 ) → ∀ 𝑛 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝐾 } ) ¬ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝐾 , 𝑛 } ⊆ 𝑒 )
23 22 nbgr0edglem ⊢ ( ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 1 ) → ( 𝐺 NeighbVtx 𝐾 ) = ∅ )
24 23 ex ⊢ ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 1 → ( 𝐺 NeighbVtx 𝐾 ) = ∅ ) )
25 df-nel ⊢ ( 𝐾 ∉ ( Vtx ‘ 𝐺 ) ↔ ¬ 𝐾 ∈ ( Vtx ‘ 𝐺 ) )
26 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
27 26 nbgrnvtx0 ⊢ ( 𝐾 ∉ ( Vtx ‘ 𝐺 ) → ( 𝐺 NeighbVtx 𝐾 ) = ∅ )
28 25 27 sylbir ⊢ ( ¬ 𝐾 ∈ ( Vtx ‘ 𝐺 ) → ( 𝐺 NeighbVtx 𝐾 ) = ∅ )
29 28 a1d ⊢ ( ¬ 𝐾 ∈ ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 1 → ( 𝐺 NeighbVtx 𝐾 ) = ∅ ) )
30 24 29 pm2.61i ⊢ ( ( ♯ ‘ ( Vtx ‘ 𝐺 ) ) = 1 → ( 𝐺 NeighbVtx 𝐾 ) = ∅ )