Theorem nbgrel

Description: Characterization of a neighbor N of a vertex X in a graph G . (Contributed by Alexander van der Vekens and Mario Carneiro, 9-Oct-2017) (Revised by AV, 26-Oct-2020) (Revised by AV, 12-Feb-2022)

	Ref	Expression
Hypotheses	nbgrel.v	|- V = ( Vtx ` G )
	nbgrel.e	|- E = ( Edg ` G )
Assertion	nbgrel	|- ( N e. ( G NeighbVtx X ) <-> ( ( N e. V /\ X e. V ) /\ N =/= X /\ E. e e. E { X , N } C_ e ) )

Proof

Step	Hyp	Ref	Expression
1		nbgrel.v	|- V = ( Vtx ` G )
2		nbgrel.e	|- E = ( Edg ` G )
3	1	nbgrcl	|- ( N e. ( G NeighbVtx X ) -> X e. V )
4	3	pm4.71ri	|- ( N e. ( G NeighbVtx X ) <-> ( X e. V /\ N e. ( G NeighbVtx X ) ) )
5	1 2	nbgrval	|- ( X e. V -> ( G NeighbVtx X ) = { n e. ( V \ { X } ) | E. e e. E { X , n } C_ e } )
6	5	eleq2d	|- ( X e. V -> ( N e. ( G NeighbVtx X ) <-> N e. { n e. ( V \ { X } ) | E. e e. E { X , n } C_ e } ) )
7		preq2	|- ( n = N -> { X , n } = { X , N } )
8	7	sseq1d	|- ( n = N -> ( { X , n } C_ e <-> { X , N } C_ e ) )
9	8	rexbidv	|- ( n = N -> ( E. e e. E { X , n } C_ e <-> E. e e. E { X , N } C_ e ) )
10	9	elrab	|- ( N e. { n e. ( V \ { X } ) | E. e e. E { X , n } C_ e } <-> ( N e. ( V \ { X } ) /\ E. e e. E { X , N } C_ e ) )
11		eldifsn	|- ( N e. ( V \ { X } ) <-> ( N e. V /\ N =/= X ) )
12	11	anbi1i	|- ( ( N e. ( V \ { X } ) /\ E. e e. E { X , N } C_ e ) <-> ( ( N e. V /\ N =/= X ) /\ E. e e. E { X , N } C_ e ) )
13	10 12	bitri	|- ( N e. { n e. ( V \ { X } ) | E. e e. E { X , n } C_ e } <-> ( ( N e. V /\ N =/= X ) /\ E. e e. E { X , N } C_ e ) )
14	6 13	bitrdi	|- ( X e. V -> ( N e. ( G NeighbVtx X ) <-> ( ( N e. V /\ N =/= X ) /\ E. e e. E { X , N } C_ e ) ) )
15	14	pm5.32i	|- ( ( X e. V /\ N e. ( G NeighbVtx X ) ) <-> ( X e. V /\ ( ( N e. V /\ N =/= X ) /\ E. e e. E { X , N } C_ e ) ) )
16		df-3an	|- ( ( ( N e. V /\ X e. V ) /\ N =/= X /\ E. e e. E { X , N } C_ e ) <-> ( ( ( N e. V /\ X e. V ) /\ N =/= X ) /\ E. e e. E { X , N } C_ e ) )
17		anass	|- ( ( ( X e. V /\ N e. V ) /\ N =/= X ) <-> ( X e. V /\ ( N e. V /\ N =/= X ) ) )
18		ancom	|- ( ( X e. V /\ N e. V ) <-> ( N e. V /\ X e. V ) )
19	18	anbi1i	|- ( ( ( X e. V /\ N e. V ) /\ N =/= X ) <-> ( ( N e. V /\ X e. V ) /\ N =/= X ) )
20	17 19	bitr3i	|- ( ( X e. V /\ ( N e. V /\ N =/= X ) ) <-> ( ( N e. V /\ X e. V ) /\ N =/= X ) )
21	20	anbi1i	|- ( ( ( X e. V /\ ( N e. V /\ N =/= X ) ) /\ E. e e. E { X , N } C_ e ) <-> ( ( ( N e. V /\ X e. V ) /\ N =/= X ) /\ E. e e. E { X , N } C_ e ) )
22		anass	|- ( ( ( X e. V /\ ( N e. V /\ N =/= X ) ) /\ E. e e. E { X , N } C_ e ) <-> ( X e. V /\ ( ( N e. V /\ N =/= X ) /\ E. e e. E { X , N } C_ e ) ) )
23	16 21 22	3bitr2ri	|- ( ( X e. V /\ ( ( N e. V /\ N =/= X ) /\ E. e e. E { X , N } C_ e ) ) <-> ( ( N e. V /\ X e. V ) /\ N =/= X /\ E. e e. E { X , N } C_ e ) )
24	15 23	bitri	|- ( ( X e. V /\ N e. ( G NeighbVtx X ) ) <-> ( ( N e. V /\ X e. V ) /\ N =/= X /\ E. e e. E { X , N } C_ e ) )
25	4 24	bitri	|- ( N e. ( G NeighbVtx X ) <-> ( ( N e. V /\ X e. V ) /\ N =/= X /\ E. e e. E { X , N } C_ e ) )