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