Metamath Proof Explorer

Theorem nbumgrvtx

Description: The set of neighbors of a vertex in a multigraph. (Contributed by AV, 27-Nov-2020) (Proof shortened by AV, 30-Dec-2020)

Ref Expression
Hypotheses nbuhgr.v 
|- V = ( Vtx ` G )
nbuhgr.e 
|- E = ( Edg ` G )
Assertion nbumgrvtx 
|- ( ( G e. UMGraph /\ N e. V ) -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } )

Proof

Step Hyp Ref Expression
1 nbuhgr.v 
 |-  V = ( Vtx ` G )
2 nbuhgr.e 
 |-  E = ( Edg ` G )
3 1 2 nbgrval 
 |-  ( N e. V -> ( G NeighbVtx N ) = { v e. ( V \ { N } ) | E. e e. E { N , v } C_ e } )
4 3 adantl 
 |-  ( ( G e. UMGraph /\ N e. V ) -> ( G NeighbVtx N ) = { v e. ( V \ { N } ) | E. e e. E { N , v } C_ e } )
5 eldifi 
 |-  ( x e. ( V \ { N } ) -> x e. V )
6 5 adantl 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) -> x e. V )
7 6 adantr 
 |-  ( ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) /\ ( e e. E /\ { N , x } C_ e ) ) -> x e. V )
8 umgrupgr 
 |-  ( G e. UMGraph -> G e. UPGraph )
9 8 ad4antr 
 |-  ( ( ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) /\ e e. E ) /\ { N , x } C_ e ) -> G e. UPGraph )
10 simpr 
 |-  ( ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) /\ e e. E ) -> e e. E )
11 10 adantr 
 |-  ( ( ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) /\ e e. E ) /\ { N , x } C_ e ) -> e e. E )
12 simpr 
 |-  ( ( ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) /\ e e. E ) /\ { N , x } C_ e ) -> { N , x } C_ e )
13 simpr 
 |-  ( ( G e. UMGraph /\ N e. V ) -> N e. V )
14 13 adantr 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) -> N e. V )
15 vex 
 |-  x e. _V
16 15 a1i 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) -> x e. _V )
17 eldifsn 
 |-  ( x e. ( V \ { N } ) <-> ( x e. V /\ x =/= N ) )
18 simpr 
 |-  ( ( x e. V /\ x =/= N ) -> x =/= N )
19 18 necomd 
 |-  ( ( x e. V /\ x =/= N ) -> N =/= x )
20 17 19 sylbi 
 |-  ( x e. ( V \ { N } ) -> N =/= x )
21 20 adantl 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) -> N =/= x )
22 14 16 21 3jca 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) -> ( N e. V /\ x e. _V /\ N =/= x ) )
23 22 adantr 
 |-  ( ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) /\ e e. E ) -> ( N e. V /\ x e. _V /\ N =/= x ) )
24 23 adantr 
 |-  ( ( ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) /\ e e. E ) /\ { N , x } C_ e ) -> ( N e. V /\ x e. _V /\ N =/= x ) )
25 1 2 upgredgpr 
 |-  ( ( ( G e. UPGraph /\ e e. E /\ { N , x } C_ e ) /\ ( N e. V /\ x e. _V /\ N =/= x ) ) -> { N , x } = e )
26 9 11 12 24 25 syl31anc 
 |-  ( ( ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) /\ e e. E ) /\ { N , x } C_ e ) -> { N , x } = e )
27 26 ex 
 |-  ( ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) /\ e e. E ) -> ( { N , x } C_ e -> { N , x } = e ) )
28 eleq1 
 |-  ( { N , x } = e -> ( { N , x } e. E <-> e e. E ) )
29 28 biimprd 
 |-  ( { N , x } = e -> ( e e. E -> { N , x } e. E ) )
30 27 10 29 syl6ci 
 |-  ( ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) /\ e e. E ) -> ( { N , x } C_ e -> { N , x } e. E ) )
31 30 impr 
 |-  ( ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) /\ ( e e. E /\ { N , x } C_ e ) ) -> { N , x } e. E )
32 7 31 jca 
 |-  ( ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) /\ ( e e. E /\ { N , x } C_ e ) ) -> ( x e. V /\ { N , x } e. E ) )
33 32 rexlimdvaa 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ x e. ( V \ { N } ) ) -> ( E. e e. E { N , x } C_ e -> ( x e. V /\ { N , x } e. E ) ) )
34 33 expimpd 
 |-  ( ( G e. UMGraph /\ N e. V ) -> ( ( x e. ( V \ { N } ) /\ E. e e. E { N , x } C_ e ) -> ( x e. V /\ { N , x } e. E ) ) )
35 simprl 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ ( x e. V /\ { N , x } e. E ) ) -> x e. V )
36 2 umgredgne 
 |-  ( ( G e. UMGraph /\ { N , x } e. E ) -> N =/= x )
37 36 ad2ant2rl 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ ( x e. V /\ { N , x } e. E ) ) -> N =/= x )
38 37 necomd 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ ( x e. V /\ { N , x } e. E ) ) -> x =/= N )
39 35 38 17 sylanbrc 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ ( x e. V /\ { N , x } e. E ) ) -> x e. ( V \ { N } ) )
40 simpr 
 |-  ( ( x e. V /\ { N , x } e. E ) -> { N , x } e. E )
41 40 adantl 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ ( x e. V /\ { N , x } e. E ) ) -> { N , x } e. E )
42 sseq2 
 |-  ( e = { N , x } -> ( { N , x } C_ e <-> { N , x } C_ { N , x } ) )
43 42 adantl 
 |-  ( ( ( ( G e. UMGraph /\ N e. V ) /\ ( x e. V /\ { N , x } e. E ) ) /\ e = { N , x } ) -> ( { N , x } C_ e <-> { N , x } C_ { N , x } ) )
44 ssidd 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ ( x e. V /\ { N , x } e. E ) ) -> { N , x } C_ { N , x } )
45 41 43 44 rspcedvd 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ ( x e. V /\ { N , x } e. E ) ) -> E. e e. E { N , x } C_ e )
46 39 45 jca 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ ( x e. V /\ { N , x } e. E ) ) -> ( x e. ( V \ { N } ) /\ E. e e. E { N , x } C_ e ) )
47 46 ex 
 |-  ( ( G e. UMGraph /\ N e. V ) -> ( ( x e. V /\ { N , x } e. E ) -> ( x e. ( V \ { N } ) /\ E. e e. E { N , x } C_ e ) ) )
48 34 47 impbid 
 |-  ( ( G e. UMGraph /\ N e. V ) -> ( ( x e. ( V \ { N } ) /\ E. e e. E { N , x } C_ e ) <-> ( x e. V /\ { N , x } e. E ) ) )
49 preq2 
 |-  ( v = x -> { N , v } = { N , x } )
50 49 sseq1d 
 |-  ( v = x -> ( { N , v } C_ e <-> { N , x } C_ e ) )
51 50 rexbidv 
 |-  ( v = x -> ( E. e e. E { N , v } C_ e <-> E. e e. E { N , x } C_ e ) )
52 51 elrab 
 |-  ( x e. { v e. ( V \ { N } ) | E. e e. E { N , v } C_ e } <-> ( x e. ( V \ { N } ) /\ E. e e. E { N , x } C_ e ) )
53 preq2 
 |-  ( n = x -> { N , n } = { N , x } )
54 53 eleq1d 
 |-  ( n = x -> ( { N , n } e. E <-> { N , x } e. E ) )
55 54 elrab 
 |-  ( x e. { n e. V | { N , n } e. E } <-> ( x e. V /\ { N , x } e. E ) )
56 48 52 55 3bitr4g 
 |-  ( ( G e. UMGraph /\ N e. V ) -> ( x e. { v e. ( V \ { N } ) | E. e e. E { N , v } C_ e } <-> x e. { n e. V | { N , n } e. E } ) )
57 56 eqrdv 
 |-  ( ( G e. UMGraph /\ N e. V ) -> { v e. ( V \ { N } ) | E. e e. E { N , v } C_ e } = { n e. V | { N , n } e. E } )
58 4 57 eqtrd 
 |-  ( ( G e. UMGraph /\ N e. V ) -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } )