Metamath Proof Explorer

Theorem nbupgr

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

Ref Expression
Hypotheses nbuhgr.v 
|- V = ( Vtx ` G )
nbuhgr.e 
|- E = ( Edg ` G )
Assertion nbupgr 
|- ( ( G e. UPGraph /\ N e. V ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | { 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 ) = { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } )
4 3 adantl 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } )
5 simp-4l 
 |-  ( ( ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) /\ e e. E ) /\ { N , n } C_ e ) -> G e. UPGraph )
6 simpr 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) /\ e e. E ) -> e e. E )
7 6 adantr 
 |-  ( ( ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) /\ e e. E ) /\ { N , n } C_ e ) -> e e. E )
8 simpr 
 |-  ( ( ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) /\ e e. E ) /\ { N , n } C_ e ) -> { N , n } C_ e )
9 simpr 
 |-  ( ( G e. UPGraph /\ N e. V ) -> N e. V )
10 9 adantr 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) -> N e. V )
11 vex 
 |-  n e. _V
12 11 a1i 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) -> n e. _V )
13 eldifsn 
 |-  ( n e. ( V \ { N } ) <-> ( n e. V /\ n =/= N ) )
14 simpr 
 |-  ( ( n e. V /\ n =/= N ) -> n =/= N )
15 14 necomd 
 |-  ( ( n e. V /\ n =/= N ) -> N =/= n )
16 13 15 sylbi 
 |-  ( n e. ( V \ { N } ) -> N =/= n )
17 16 adantl 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) -> N =/= n )
18 10 12 17 3jca 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) -> ( N e. V /\ n e. _V /\ N =/= n ) )
19 18 adantr 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) /\ e e. E ) -> ( N e. V /\ n e. _V /\ N =/= n ) )
20 19 adantr 
 |-  ( ( ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) /\ e e. E ) /\ { N , n } C_ e ) -> ( N e. V /\ n e. _V /\ N =/= n ) )
21 1 2 upgredgpr 
 |-  ( ( ( G e. UPGraph /\ e e. E /\ { N , n } C_ e ) /\ ( N e. V /\ n e. _V /\ N =/= n ) ) -> { N , n } = e )
22 5 7 8 20 21 syl31anc 
 |-  ( ( ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) /\ e e. E ) /\ { N , n } C_ e ) -> { N , n } = e )
23 22 ex 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) /\ e e. E ) -> ( { N , n } C_ e -> { N , n } = e ) )
24 eleq1 
 |-  ( { N , n } = e -> ( { N , n } e. E <-> e e. E ) )
25 24 biimprd 
 |-  ( { N , n } = e -> ( e e. E -> { N , n } e. E ) )
26 23 6 25 syl6ci 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) /\ e e. E ) -> ( { N , n } C_ e -> { N , n } e. E ) )
27 26 rexlimdva 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) -> ( E. e e. E { N , n } C_ e -> { N , n } e. E ) )
28 simpr 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) /\ { N , n } e. E ) -> { N , n } e. E )
29 sseq2 
 |-  ( e = { N , n } -> ( { N , n } C_ e <-> { N , n } C_ { N , n } ) )
30 29 adantl 
 |-  ( ( ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) /\ { N , n } e. E ) /\ e = { N , n } ) -> ( { N , n } C_ e <-> { N , n } C_ { N , n } ) )
31 ssidd 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) /\ { N , n } e. E ) -> { N , n } C_ { N , n } )
32 28 30 31 rspcedvd 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) /\ { N , n } e. E ) -> E. e e. E { N , n } C_ e )
33 32 ex 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) -> ( { N , n } e. E -> E. e e. E { N , n } C_ e ) )
34 27 33 impbid 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ n e. ( V \ { N } ) ) -> ( E. e e. E { N , n } C_ e <-> { N , n } e. E ) )
35 34 rabbidva 
 |-  ( ( G e. UPGraph /\ N e. V ) -> { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } = { n e. ( V \ { N } ) | { N , n } e. E } )
36 4 35 eqtrd 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | { N , n } e. E } )