This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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