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 nbgr0vtxlem ( ( 𝐾 ∈ ( 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 𝐾 ) = ∅ )