Theorem dfnbgr3 39418

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

Hypotheses

Ref	Expression
dfnbgr3.v	|- V = (Vtx ` G )
dfnbgr3.i	|- I = (iEdg ` G )

Assertion

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

Distinct variable groups:   n, G   i, I, n   i, N, n   n, V   n, W

Allowed substitution hints:   G( i)   V( i)   W( i)

Proof of Theorem dfnbgr3

Dummy variable e is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfnbgr3.v	. . . 4 |- V = (Vtx ` G )
2		eqid 2453	. . . 4 |- (Edg ` G ) = (Edg ` G )
3	1, 2	nbgrval 39416	. . 3 |- ( ( G e. W /\ N e. V ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. (Edg ` G ) { N , n } C_ e } )
4	3	3adant3 1029	. 2 |- ( ( G e. W /\ N e. V /\ Fun I ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. (Edg ` G ) { N , n } C_ e } )
5		edgaval 39222	. . . . . . 7 |- ( G e. W -> (Edg ` G ) = ran (iEdg ` G ) )
6		dfnbgr3.i	. . . . . . . . 9 |- I = (iEdg ` G )
7	6	eqcomi 2462	. . . . . . . 8 |- (iEdg ` G ) = I
8	7	rneqi 5064	. . . . . . 7 |- ran (iEdg ` G ) = ran I
9	5, 8	syl6eq 2503	. . . . . 6 |- ( G e. W -> (Edg ` G ) = ran I )
10	9	rexeqdv 2996	. . . . 5 |- ( G e. W -> ( E. e e. (Edg ` G ) { N , n } C_ e <-> E. e e. ran I { N , n } C_ e ) )
11	10	3ad2ant1 1030	. . . 4 |- ( ( G e. W /\ N e. V /\ Fun I ) -> ( E. e e. (Edg ` G ) { N , n } C_ e <-> E. e e. ran I { N , n } C_ e ) )
12		funfn 5614	. . . . . . 7 |- ( Fun I <-> I Fn dom I )
13	12	biimpi 198	. . . . . 6 |- ( Fun I -> I Fn dom I )
14	13	3ad2ant3 1032	. . . . 5 |- ( ( G e. W /\ N e. V /\ Fun I ) -> I Fn dom I )
15		sseq2 3456	. . . . . 6 |- ( e = ( I ` i ) -> ( { N , n } C_ e <-> { N , n } C_ ( I ` i ) ) )
16	15	rexrn 6029	. . . . 5 |- ( I Fn dom I -> ( E. e e. ran I { N , n } C_ e <-> E. i e. dom I { N , n } C_ ( I ` i ) ) )
17	14, 16	syl 17	. . . 4 |- ( ( G e. W /\ N e. V /\ Fun I ) -> ( E. e e. ran I { N , n } C_ e <-> E. i e. dom I { N , n } C_ ( I ` i ) ) )
18	11, 17	bitrd 257	. . 3 |- ( ( G e. W /\ N e. V /\ Fun I ) -> ( E. e e. (Edg ` G ) { N , n } C_ e <-> E. i e. dom I { N , n } C_ ( I ` i ) ) )
19	18	rabbidv 3038	. 2 |- ( ( G e. W /\ 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 ) } )
20	4, 19	eqtrd 2487	1 |- ( ( G e. W /\ N e. V /\ Fun I ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. i e. dom I { N , n } C_ ( I ` i ) } )

Syntax hints:   -> wi 4   <-> wb 188   /\ w3a 986   = wceq 1446   e. wcel 1889   E.wrex 2740   {crab 2743   \ cdif 3403   C_ wss 3406   {csn 3970   {cpr 3972   dom cdm 4837   ran crn 4838   Fun wfun 5579   Fn wfn 5580   ` cfv 5585  (class class class)co 6295  Vtxcvtx 39111  iEdgciedg 39112  Edgcedga 39220   NeighbVtx cnbgr 39407

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642  ax-un 6588

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-mpt 4466  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-iota 5549  df-fun 5587  df-fn 5588  df-fv 5593  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-edga 39221  df-nbgr 39411

This theorem is referenced by: (None)