Theorem dfnbgr3

Description: Alternate definition of the neighbors of a vertex using the edge function instead of the edges themselves (see also nbgrval ). (Contributed by Alexander van der Vekens, 17-Dec-2017) (Revised by AV, 25-Oct-2020) (Revised by AV, 21-Mar-2021)

	Ref	Expression
Hypotheses	dfnbgr3.v	|- V = ( Vtx ` G )
	dfnbgr3.i	|- I = ( iEdg ` G )
Assertion	dfnbgr3	|- ( ( N e. V /\ Fun I ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. i e. dom I { N , n } C_ ( I ` i ) } )

Proof

Step	Hyp	Ref	Expression
1		dfnbgr3.v	|- V = ( Vtx ` G )
2		dfnbgr3.i	|- I = ( iEdg ` G )
3		eqid	|- ( Edg ` G ) = ( Edg ` G )
4	1 3	nbgrval	|- ( N e. V -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. ( Edg ` G ) { N , n } C_ e } )
5	4	adantr	|- ( ( N e. V /\ Fun I ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. ( Edg ` G ) { N , n } C_ e } )
6		edgval	|- ( Edg ` G ) = ran ( iEdg ` G )
7	2	eqcomi	|- ( iEdg ` G ) = I
8	7	rneqi	|- ran ( iEdg ` G ) = ran I
9	6 8	eqtri	|- ( Edg ` G ) = ran I
10	9	rexeqi	|- ( E. e e. ( Edg ` G ) { N , n } C_ e <-> E. e e. ran I { N , n } C_ e )
11		funfn	|- ( Fun I <-> I Fn dom I )
12	11	biimpi	|- ( Fun I -> I Fn dom I )
13	12	adantl	|- ( ( N e. V /\ Fun I ) -> I Fn dom I )
14		sseq2	|- ( e = ( I ` i ) -> ( { N , n } C_ e <-> { N , n } C_ ( I ` i ) ) )
15	14	rexrn	|- ( I Fn dom I -> ( E. e e. ran I { N , n } C_ e <-> E. i e. dom I { N , n } C_ ( I ` i ) ) )
16	13 15	syl	|- ( ( N e. V /\ Fun I ) -> ( E. e e. ran I { N , n } C_ e <-> E. i e. dom I { N , n } C_ ( I ` i ) ) )
17	10 16	syl5bb	|- ( ( N e. V /\ Fun I ) -> ( E. e e. ( Edg ` G ) { N , n } C_ e <-> E. i e. dom I { N , n } C_ ( I ` i ) ) )
18	17	rabbidv	|- ( ( N e. V /\ Fun I ) -> { n e. ( V \ { N } ) | E. e e. ( Edg ` G ) { N , n } C_ e } = { n e. ( V \ { N } ) | E. i e. dom I { N , n } C_ ( I ` i ) } )
19	5 18	eqtrd	|- ( ( N e. V /\ Fun I ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. i e. dom I { N , n } C_ ( I ` i ) } )