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 USGraph N G NeighbVtx K I I -1 K N = K N

Proof

Step Hyp Ref Expression
1 usgrnbcnvfv.i I = iEdg G
2 1 usgrf1o G 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 USGraph N G NeighbVtx K N K 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 USGraph Edg G = ran I
11 10 eleq2d G USGraph N K Edg G N K ran I
12 5 11 bitrd G USGraph N G NeighbVtx K N K ran I
13 12 biimpa G USGraph N G NeighbVtx K N K ran I
14 3 13 eqeltrrid G USGraph N G NeighbVtx K K N ran I
15 f1ocnvfv2 I : dom I 1-1 onto ran I K N ran I I I -1 K N = K N
16 2 14 15 syl2an2r G USGraph N G NeighbVtx K I I -1 K N = K N