Metamath Proof Explorer

Theorem nbuhgr

Description: The set of neighbors of a vertex in a hypergraph. This version of nbgrval (with N being an arbitrary set instead of being a vertex) only holds for classes whose edges are subsets of the set of vertices (hypergraphs!). (Contributed by AV, 26-Oct-2020) (Proof shortened by AV, 15-Nov-2020)

Ref Expression
Hypotheses nbuhgr.v 
|- V = ( Vtx ` G )
nbuhgr.e 
|- E = ( Edg ` G )
Assertion nbuhgr 
|- ( ( G e. UHGraph /\ N e. X ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E { N , n } C_ 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 a1d 
 |-  ( N e. V -> ( ( G e. UHGraph /\ N e. X ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } ) )
5 df-nel 
 |-  ( N e/ V <-> -. N e. V )
6 1 nbgrnvtx0 
 |-  ( N e/ V -> ( G NeighbVtx N ) = (/) )
7 5 6 sylbir 
 |-  ( -. N e. V -> ( G NeighbVtx N ) = (/) )
8 7 adantr 
 |-  ( ( -. N e. V /\ ( G e. UHGraph /\ N e. X ) ) -> ( G NeighbVtx N ) = (/) )
9 simpl 
 |-  ( ( G e. UHGraph /\ N e. X ) -> G e. UHGraph )
10 9 adantr 
 |-  ( ( ( G e. UHGraph /\ N e. X ) /\ n e. ( V \ { N } ) ) -> G e. UHGraph )
11 2 eleq2i 
 |-  ( e e. E <-> e e. ( Edg ` G ) )
12 11 biimpi 
 |-  ( e e. E -> e e. ( Edg ` G ) )
13 edguhgr 
 |-  ( ( G e. UHGraph /\ e e. ( Edg ` G ) ) -> e e. ~P ( Vtx ` G ) )
14 10 12 13 syl2an 
 |-  ( ( ( ( G e. UHGraph /\ N e. X ) /\ n e. ( V \ { N } ) ) /\ e e. E ) -> e e. ~P ( Vtx ` G ) )
15 velpw 
 |-  ( e e. ~P ( Vtx ` G ) <-> e C_ ( Vtx ` G ) )
16 1 eqcomi 
 |-  ( Vtx ` G ) = V
17 16 sseq2i 
 |-  ( e C_ ( Vtx ` G ) <-> e C_ V )
18 15 17 bitri 
 |-  ( e e. ~P ( Vtx ` G ) <-> e C_ V )
19 sstr 
 |-  ( ( { N , n } C_ e /\ e C_ V ) -> { N , n } C_ V )
20 prssg 
 |-  ( ( N e. X /\ n e. _V ) -> ( ( N e. V /\ n e. V ) <-> { N , n } C_ V ) )
21 20 bicomd 
 |-  ( ( N e. X /\ n e. _V ) -> ( { N , n } C_ V <-> ( N e. V /\ n e. V ) ) )
22 21 elvd 
 |-  ( N e. X -> ( { N , n } C_ V <-> ( N e. V /\ n e. V ) ) )
23 simpl 
 |-  ( ( N e. V /\ n e. V ) -> N e. V )
24 22 23 biimtrdi 
 |-  ( N e. X -> ( { N , n } C_ V -> N e. V ) )
25 19 24 syl5com 
 |-  ( ( { N , n } C_ e /\ e C_ V ) -> ( N e. X -> N e. V ) )
26 25 ex 
 |-  ( { N , n } C_ e -> ( e C_ V -> ( N e. X -> N e. V ) ) )
27 26 com13 
 |-  ( N e. X -> ( e C_ V -> ( { N , n } C_ e -> N e. V ) ) )
28 27 ad3antlr 
 |-  ( ( ( ( G e. UHGraph /\ N e. X ) /\ n e. ( V \ { N } ) ) /\ e e. E ) -> ( e C_ V -> ( { N , n } C_ e -> N e. V ) ) )
29 18 28 biimtrid 
 |-  ( ( ( ( G e. UHGraph /\ N e. X ) /\ n e. ( V \ { N } ) ) /\ e e. E ) -> ( e e. ~P ( Vtx ` G ) -> ( { N , n } C_ e -> N e. V ) ) )
30 14 29 mpd 
 |-  ( ( ( ( G e. UHGraph /\ N e. X ) /\ n e. ( V \ { N } ) ) /\ e e. E ) -> ( { N , n } C_ e -> N e. V ) )
31 30 rexlimdva 
 |-  ( ( ( G e. UHGraph /\ N e. X ) /\ n e. ( V \ { N } ) ) -> ( E. e e. E { N , n } C_ e -> N e. V ) )
32 31 con3rr3 
 |-  ( -. N e. V -> ( ( ( G e. UHGraph /\ N e. X ) /\ n e. ( V \ { N } ) ) -> -. E. e e. E { N , n } C_ e ) )
33 32 expdimp 
 |-  ( ( -. N e. V /\ ( G e. UHGraph /\ N e. X ) ) -> ( n e. ( V \ { N } ) -> -. E. e e. E { N , n } C_ e ) )
34 33 ralrimiv 
 |-  ( ( -. N e. V /\ ( G e. UHGraph /\ N e. X ) ) -> A. n e. ( V \ { N } ) -. E. e e. E { N , n } C_ e )
35 rabeq0 
 |-  ( { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } = (/) <-> A. n e. ( V \ { N } ) -. E. e e. E { N , n } C_ e )
36 34 35 sylibr 
 |-  ( ( -. N e. V /\ ( G e. UHGraph /\ N e. X ) ) -> { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } = (/) )
37 8 36 eqtr4d 
 |-  ( ( -. N e. V /\ ( G e. UHGraph /\ N e. X ) ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } )
38 37 ex 
 |-  ( -. N e. V -> ( ( G e. UHGraph /\ N e. X ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } ) )
39 4 38 pm2.61i 
 |-  ( ( G e. UHGraph /\ N e. X ) -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } )