Step |
Hyp |
Ref |
Expression |
1 |
|
nbusgreledg.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
2 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
3 |
2 1
|
nbusgr |
⊢ ( 𝐺 ∈ USGraph → ( 𝐺 NeighbVtx 𝐾 ) = { 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) |
4 |
3
|
eleq2d |
⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ 𝑁 ∈ { 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) ) |
5 |
1 2
|
usgrpredgv |
⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) → ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) |
6 |
5
|
simprd |
⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) → 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) |
7 |
6
|
ex |
⊢ ( 𝐺 ∈ USGraph → ( { 𝐾 , 𝑁 } ∈ 𝐸 → 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) |
8 |
7
|
pm4.71rd |
⊢ ( 𝐺 ∈ USGraph → ( { 𝐾 , 𝑁 } ∈ 𝐸 ↔ ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) ) |
9 |
|
prcom |
⊢ { 𝑁 , 𝐾 } = { 𝐾 , 𝑁 } |
10 |
9
|
eleq1i |
⊢ ( { 𝑁 , 𝐾 } ∈ 𝐸 ↔ { 𝐾 , 𝑁 } ∈ 𝐸 ) |
11 |
10
|
a1i |
⊢ ( 𝐺 ∈ USGraph → ( { 𝑁 , 𝐾 } ∈ 𝐸 ↔ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) |
12 |
|
preq2 |
⊢ ( 𝑛 = 𝑁 → { 𝐾 , 𝑛 } = { 𝐾 , 𝑁 } ) |
13 |
12
|
eleq1d |
⊢ ( 𝑛 = 𝑁 → ( { 𝐾 , 𝑛 } ∈ 𝐸 ↔ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) |
14 |
13
|
elrab |
⊢ ( 𝑁 ∈ { 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ↔ ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) |
15 |
14
|
a1i |
⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ∈ { 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ↔ ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) ) |
16 |
8 11 15
|
3bitr4rd |
⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ∈ { 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ↔ { 𝑁 , 𝐾 } ∈ 𝐸 ) ) |
17 |
4 16
|
bitrd |
⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ { 𝑁 , 𝐾 } ∈ 𝐸 ) ) |