Step |
Hyp |
Ref |
Expression |
1 |
|
nbgrnself.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
neldifsnd |
⊢ ( 𝑣 ∈ 𝑉 → ¬ 𝑣 ∈ ( 𝑉 ∖ { 𝑣 } ) ) |
3 |
2
|
intnanrd |
⊢ ( 𝑣 ∈ 𝑉 → ¬ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑣 } ) ∧ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑣 } ⊆ 𝑒 ) ) |
4 |
|
df-nel |
⊢ ( 𝑣 ∉ { 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ↔ ¬ 𝑣 ∈ { 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ) |
5 |
|
preq2 |
⊢ ( 𝑛 = 𝑣 → { 𝑣 , 𝑛 } = { 𝑣 , 𝑣 } ) |
6 |
5
|
sseq1d |
⊢ ( 𝑛 = 𝑣 → ( { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ { 𝑣 , 𝑣 } ⊆ 𝑒 ) ) |
7 |
6
|
rexbidv |
⊢ ( 𝑛 = 𝑣 → ( ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑣 } ⊆ 𝑒 ) ) |
8 |
7
|
elrab |
⊢ ( 𝑣 ∈ { 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ↔ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑣 } ) ∧ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑣 } ⊆ 𝑒 ) ) |
9 |
4 8
|
xchbinx |
⊢ ( 𝑣 ∉ { 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ↔ ¬ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑣 } ) ∧ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑣 } ⊆ 𝑒 ) ) |
10 |
3 9
|
sylibr |
⊢ ( 𝑣 ∈ 𝑉 → 𝑣 ∉ { 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ) |
11 |
|
eqidd |
⊢ ( 𝑣 ∈ 𝑉 → 𝑣 = 𝑣 ) |
12 |
|
eqid |
⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) |
13 |
1 12
|
nbgrval |
⊢ ( 𝑣 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑣 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ) |
14 |
11 13
|
neleq12d |
⊢ ( 𝑣 ∈ 𝑉 → ( 𝑣 ∉ ( 𝐺 NeighbVtx 𝑣 ) ↔ 𝑣 ∉ { 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ∣ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑣 , 𝑛 } ⊆ 𝑒 } ) ) |
15 |
10 14
|
mpbird |
⊢ ( 𝑣 ∈ 𝑉 → 𝑣 ∉ ( 𝐺 NeighbVtx 𝑣 ) ) |
16 |
15
|
rgen |
⊢ ∀ 𝑣 ∈ 𝑉 𝑣 ∉ ( 𝐺 NeighbVtx 𝑣 ) |