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 } )