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 
|- I = ( iEdg ` G )
Assertion usgrnbcnvfv 
|- ( ( G e. USGraph /\ N e. ( G NeighbVtx K ) ) -> ( I ` ( `' I ` { K , N } ) ) = { K , N } )

Proof

Step Hyp Ref Expression
1 usgrnbcnvfv.i 
 |-  I = ( iEdg ` G )
2 1 usgrf1o 
 |-  ( G e. USGraph -> I : dom I -1-1-onto-> ran I )
3 prcom 
 |-  { N , K } = { K , N }
4 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
5 4 nbusgreledg 
 |-  ( G e. USGraph -> ( N e. ( G NeighbVtx K ) <-> { N , K } e. ( Edg ` G ) ) )
6 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
7 1 eqcomi 
 |-  ( iEdg ` G ) = I
8 7 rneqi 
 |-  ran ( iEdg ` G ) = ran I
9 6 8 eqtri 
 |-  ( Edg ` G ) = ran I
10 9 a1i 
 |-  ( G e. USGraph -> ( Edg ` G ) = ran I )
11 10 eleq2d 
 |-  ( G e. USGraph -> ( { N , K } e. ( Edg ` G ) <-> { N , K } e. ran I ) )
12 5 11 bitrd 
 |-  ( G e. USGraph -> ( N e. ( G NeighbVtx K ) <-> { N , K } e. ran I ) )
13 12 biimpa 
 |-  ( ( G e. USGraph /\ N e. ( G NeighbVtx K ) ) -> { N , K } e. ran I )
14 3 13 eqeltrrid 
 |-  ( ( G e. USGraph /\ N e. ( G NeighbVtx K ) ) -> { K , N } e. ran I )
15 f1ocnvfv2 
 |-  ( ( I : dom I -1-1-onto-> ran I /\ { K , N } e. ran I ) -> ( I ` ( `' I ` { K , N } ) ) = { K , N } )
16 2 14 15 syl2an2r 
 |-  ( ( G e. USGraph /\ N e. ( G NeighbVtx K ) ) -> ( I ` ( `' I ` { K , N } ) ) = { K , N } )