Metamath Proof Explorer

Theorem dfclnbgr6

Description: Alternate definition of the closed neighborhood of a vertex as union of the vertex with its semiopen neighborhood. (Contributed by AV, 17-May-2025)

Ref Expression
Hypotheses dfvopnbgr2.v 
|- V = ( Vtx ` G )
dfvopnbgr2.e 
|- E = ( Edg ` G )
dfvopnbgr2.u 
|- U = { n e. V | ( n e. ( G NeighbVtx N ) \/ E. e e. E ( N = n /\ e = { N } ) ) }
Assertion dfclnbgr6 
|- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. U ) )

Proof

Step Hyp Ref Expression
1 dfvopnbgr2.v 
 |-  V = ( Vtx ` G )
2 dfvopnbgr2.e 
 |-  E = ( Edg ` G )
3 dfvopnbgr2.u 
 |-  U = { n e. V | ( n e. ( G NeighbVtx N ) \/ E. e e. E ( N = n /\ e = { N } ) ) }
4 orc 
 |-  ( v = N -> ( v = N \/ ( ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) <-> ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) ) ) )
5 4 a1d 
 |-  ( v = N -> ( N e. V -> ( v = N \/ ( ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) <-> ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) ) ) ) )
6 simpl 
 |-  ( ( v =/= N /\ N e. V ) -> v =/= N )
7 6 anim1i 
 |-  ( ( ( v =/= N /\ N e. V ) /\ ( N e. e /\ v e. e ) ) -> ( v =/= N /\ ( N e. e /\ v e. e ) ) )
8 3anass 
 |-  ( ( v =/= N /\ N e. e /\ v e. e ) <-> ( v =/= N /\ ( N e. e /\ v e. e ) ) )
9 7 8 sylibr 
 |-  ( ( ( v =/= N /\ N e. V ) /\ ( N e. e /\ v e. e ) ) -> ( v =/= N /\ N e. e /\ v e. e ) )
10 9 orcd 
 |-  ( ( ( v =/= N /\ N e. V ) /\ ( N e. e /\ v e. e ) ) -> ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) )
11 10 ex 
 |-  ( ( v =/= N /\ N e. V ) -> ( ( N e. e /\ v e. e ) -> ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) )
12 3simpc 
 |-  ( ( v =/= N /\ N e. e /\ v e. e ) -> ( N e. e /\ v e. e ) )
13 12 a1i 
 |-  ( ( v =/= N /\ N e. V ) -> ( ( v =/= N /\ N e. e /\ v e. e ) -> ( N e. e /\ v e. e ) ) )
14 vsnid 
 |-  v e. { v }
15 eleq2 
 |-  ( e = { v } -> ( v e. e <-> v e. { v } ) )
16 14 15 mpbiri 
 |-  ( e = { v } -> v e. e )
17 16 adantl 
 |-  ( ( v = N /\ e = { v } ) -> v e. e )
18 eleq1 
 |-  ( v = N -> ( v e. e <-> N e. e ) )
19 18 adantr 
 |-  ( ( v = N /\ e = { v } ) -> ( v e. e <-> N e. e ) )
20 17 19 mpbid 
 |-  ( ( v = N /\ e = { v } ) -> N e. e )
21 20 17 jca 
 |-  ( ( v = N /\ e = { v } ) -> ( N e. e /\ v e. e ) )
22 21 a1i 
 |-  ( ( v =/= N /\ N e. V ) -> ( ( v = N /\ e = { v } ) -> ( N e. e /\ v e. e ) ) )
23 13 22 jaod 
 |-  ( ( v =/= N /\ N e. V ) -> ( ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) -> ( N e. e /\ v e. e ) ) )
24 11 23 impbid 
 |-  ( ( v =/= N /\ N e. V ) -> ( ( N e. e /\ v e. e ) <-> ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) )
25 24 rexbidv 
 |-  ( ( v =/= N /\ N e. V ) -> ( E. e e. E ( N e. e /\ v e. e ) <-> E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) )
26 25 anbi2d 
 |-  ( ( v =/= N /\ N e. V ) -> ( ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) <-> ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) ) )
27 26 olcd 
 |-  ( ( v =/= N /\ N e. V ) -> ( v = N \/ ( ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) <-> ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) ) ) )
28 27 ex 
 |-  ( v =/= N -> ( N e. V -> ( v = N \/ ( ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) <-> ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) ) ) ) )
29 5 28 pm2.61ine 
 |-  ( N e. V -> ( v = N \/ ( ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) <-> ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) ) ) )
30 orbidi 
 |-  ( ( v = N \/ ( ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) <-> ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) ) ) <-> ( ( v = N \/ ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) ) <-> ( v = N \/ ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) ) ) )
31 29 30 sylib 
 |-  ( N e. V -> ( ( v = N \/ ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) ) <-> ( v = N \/ ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) ) ) )
32 elun 
 |-  ( v e. ( { N } u. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) <-> ( v e. { N } \/ v e. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) )
33 velsn 
 |-  ( v e. { N } <-> v = N )
34 eleq1 
 |-  ( n = v -> ( n e. e <-> v e. e ) )
35 34 anbi2d 
 |-  ( n = v -> ( ( N e. e /\ n e. e ) <-> ( N e. e /\ v e. e ) ) )
36 35 rexbidv 
 |-  ( n = v -> ( E. e e. E ( N e. e /\ n e. e ) <-> E. e e. E ( N e. e /\ v e. e ) ) )
37 36 elrab 
 |-  ( v e. { n e. V | E. e e. E ( N e. e /\ n e. e ) } <-> ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) )
38 33 37 orbi12i 
 |-  ( ( v e. { N } \/ v e. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) <-> ( v = N \/ ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) ) )
39 32 38 bitri 
 |-  ( v e. ( { N } u. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) <-> ( v = N \/ ( v e. V /\ E. e e. E ( N e. e /\ v e. e ) ) ) )
40 elun 
 |-  ( v e. ( { N } u. { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } ) <-> ( v e. { N } \/ v e. { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } ) )
41 neeq1 
 |-  ( n = v -> ( n =/= N <-> v =/= N ) )
42 41 34 3anbi13d 
 |-  ( n = v -> ( ( n =/= N /\ N e. e /\ n e. e ) <-> ( v =/= N /\ N e. e /\ v e. e ) ) )
43 eqeq1 
 |-  ( n = v -> ( n = N <-> v = N ) )
44 sneq 
 |-  ( n = v -> { n } = { v } )
45 44 eqeq2d 
 |-  ( n = v -> ( e = { n } <-> e = { v } ) )
46 43 45 anbi12d 
 |-  ( n = v -> ( ( n = N /\ e = { n } ) <-> ( v = N /\ e = { v } ) ) )
47 42 46 orbi12d 
 |-  ( n = v -> ( ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) <-> ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) )
48 47 rexbidv 
 |-  ( n = v -> ( E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) <-> E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) )
49 48 elrab 
 |-  ( v e. { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } <-> ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) )
50 33 49 orbi12i 
 |-  ( ( v e. { N } \/ v e. { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } ) <-> ( v = N \/ ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) ) )
51 40 50 bitri 
 |-  ( v e. ( { N } u. { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } ) <-> ( v = N \/ ( v e. V /\ E. e e. E ( ( v =/= N /\ N e. e /\ v e. e ) \/ ( v = N /\ e = { v } ) ) ) ) )
52 31 39 51 3bitr4g 
 |-  ( N e. V -> ( v e. ( { N } u. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) <-> v e. ( { N } u. { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } ) ) )
53 52 eqrdv 
 |-  ( N e. V -> ( { N } u. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) = ( { N } u. { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } ) )
54 1 2 dfclnbgr2 
 |-  ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) )
55 1 2 3 dfvopnbgr2 
 |-  ( N e. V -> U = { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } )
56 55 uneq2d 
 |-  ( N e. V -> ( { N } u. U ) = ( { N } u. { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } ) )
57 53 54 56 3eqtr4d 
 |-  ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. U ) )