Metamath Proof Explorer


Theorem usgrnbcnvfv

Description: Applying the edge function on the converse edge function applied on a pair of a vertex and one of its neighbors is this pair in a simple graph. (Contributed by Alexander van der Vekens, 18-Dec-2017) (Revised by AV, 27-Oct-2020)

Ref Expression
Hypothesis usgrnbcnvfv.i 𝐼 = ( iEdg ‘ 𝐺 )
Assertion usgrnbcnvfv ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ ( 𝐺 NeighbVtx 𝐾 ) ) → ( 𝐼 ‘ ( 𝐼 ‘ { 𝐾 , 𝑁 } ) ) = { 𝐾 , 𝑁 } )

Proof

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 𝐾 ) ) → ( 𝐼 ‘ ( 𝐼 ‘ { 𝐾 , 𝑁 } ) ) = { 𝐾 , 𝑁 } )