Step |
Hyp |
Ref |
Expression |
1 |
|
usgrnbcnvfv.i |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
2 |
1
|
usgrf1o |
⊢ ( 𝐺 ∈ USGraph → 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 ) |
3 |
|
prcom |
⊢ { 𝑁 , 𝐾 } = { 𝐾 , 𝑁 } |
4 |
|
eqid |
⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) |
5 |
4
|
nbusgreledg |
⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ { 𝑁 , 𝐾 } ∈ ( Edg ‘ 𝐺 ) ) ) |
6 |
|
edgval |
⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) |
7 |
1
|
eqcomi |
⊢ ( iEdg ‘ 𝐺 ) = 𝐼 |
8 |
7
|
rneqi |
⊢ ran ( iEdg ‘ 𝐺 ) = ran 𝐼 |
9 |
6 8
|
eqtri |
⊢ ( Edg ‘ 𝐺 ) = ran 𝐼 |
10 |
9
|
a1i |
⊢ ( 𝐺 ∈ USGraph → ( Edg ‘ 𝐺 ) = ran 𝐼 ) |
11 |
10
|
eleq2d |
⊢ ( 𝐺 ∈ USGraph → ( { 𝑁 , 𝐾 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑁 , 𝐾 } ∈ ran 𝐼 ) ) |
12 |
5 11
|
bitrd |
⊢ ( 𝐺 ∈ USGraph → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ { 𝑁 , 𝐾 } ∈ ran 𝐼 ) ) |
13 |
12
|
biimpa |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ) → { 𝑁 , 𝐾 } ∈ ran 𝐼 ) |
14 |
3 13
|
eqeltrrid |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ) → { 𝐾 , 𝑁 } ∈ ran 𝐼 ) |
15 |
|
f1ocnvfv2 |
⊢ ( ( 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 ∧ { 𝐾 , 𝑁 } ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ { 𝐾 , 𝑁 } ) ) = { 𝐾 , 𝑁 } ) |
16 |
2 14 15
|
syl2an2r |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ { 𝐾 , 𝑁 } ) ) = { 𝐾 , 𝑁 } ) |