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