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