Step |
Hyp |
Ref |
Expression |
1 |
|
clnbuhgr.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
clnbuhgr.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
1 2
|
clnbupgr |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) → ( 𝐺 ClNeighbVtx 𝐾 ) = ( { 𝐾 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) ) |
4 |
3
|
eleq2d |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) → ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ↔ 𝑁 ∈ ( { 𝐾 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) ) ) |
5 |
4
|
3adant3 |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ↔ 𝑁 ∈ ( { 𝐾 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) ) ) |
6 |
|
elun |
⊢ ( 𝑁 ∈ ( { 𝐾 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) ↔ ( 𝑁 ∈ { 𝐾 } ∨ 𝑁 ∈ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) ) |
7 |
|
preq2 |
⊢ ( 𝑛 = 𝑁 → { 𝐾 , 𝑛 } = { 𝐾 , 𝑁 } ) |
8 |
7
|
eleq1d |
⊢ ( 𝑛 = 𝑁 → ( { 𝐾 , 𝑛 } ∈ 𝐸 ↔ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) |
9 |
8
|
elrab |
⊢ ( 𝑁 ∈ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ↔ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) |
10 |
9
|
orbi2i |
⊢ ( ( 𝑁 ∈ { 𝐾 } ∨ 𝑁 ∈ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) ↔ ( 𝑁 ∈ { 𝐾 } ∨ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) ) |
11 |
6 10
|
bitri |
⊢ ( 𝑁 ∈ ( { 𝐾 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) ↔ ( 𝑁 ∈ { 𝐾 } ∨ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) ) |
12 |
|
elsng |
⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∈ { 𝐾 } ↔ 𝑁 = 𝐾 ) ) |
13 |
12
|
3ad2ant3 |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∈ { 𝐾 } ↔ 𝑁 = 𝐾 ) ) |
14 |
13
|
orbi1d |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑁 ∈ { 𝐾 } ∨ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) ↔ ( 𝑁 = 𝐾 ∨ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) ) ) |
15 |
11 14
|
bitrid |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∈ ( { 𝐾 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) ↔ ( 𝑁 = 𝐾 ∨ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) ) ) |
16 |
|
ibar |
⊢ ( 𝑁 ∈ 𝑉 → ( { 𝐾 , 𝑁 } ∈ 𝐸 ↔ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) ) |
17 |
|
prcom |
⊢ { 𝐾 , 𝑁 } = { 𝑁 , 𝐾 } |
18 |
17
|
eleq1i |
⊢ ( { 𝐾 , 𝑁 } ∈ 𝐸 ↔ { 𝑁 , 𝐾 } ∈ 𝐸 ) |
19 |
16 18
|
bitr3di |
⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ↔ { 𝑁 , 𝐾 } ∈ 𝐸 ) ) |
20 |
19
|
orbi2d |
⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑁 = 𝐾 ∨ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) ↔ ( 𝑁 = 𝐾 ∨ { 𝑁 , 𝐾 } ∈ 𝐸 ) ) ) |
21 |
20
|
3ad2ant3 |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑁 = 𝐾 ∨ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) ↔ ( 𝑁 = 𝐾 ∨ { 𝑁 , 𝐾 } ∈ 𝐸 ) ) ) |
22 |
5 15 21
|
3bitrd |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ↔ ( 𝑁 = 𝐾 ∨ { 𝑁 , 𝐾 } ∈ 𝐸 ) ) ) |