Metamath Proof Explorer

Theorem dfvopnbgr2

Description: Alternate definition of the semiopen neighborhood of a vertex breaking up the subset relationship of an unordered pair. Asemiopen neighborhood U of a vertex N is its open neighborhood together with itself if there is a loop at this vertex. (Contributed by AV, 15-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 dfvopnbgr2 
|- ( N e. V -> U = { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } )

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 1 2 nbgrel 
 |-  ( n e. ( G NeighbVtx N ) <-> ( ( n e. V /\ N e. V ) /\ n =/= N /\ E. e e. E { N , n } C_ e ) )
5 4 a1i 
 |-  ( ( N e. V /\ n e. V ) -> ( n e. ( G NeighbVtx N ) <-> ( ( n e. V /\ N e. V ) /\ n =/= N /\ E. e e. E { N , n } C_ e ) ) )
6 5 orbi1d 
 |-  ( ( N e. V /\ n e. V ) -> ( ( n e. ( G NeighbVtx N ) \/ E. e e. E ( N = n /\ e = { N } ) ) <-> ( ( ( n e. V /\ N e. V ) /\ n =/= N /\ E. e e. E { N , n } C_ e ) \/ E. e e. E ( N = n /\ e = { N } ) ) ) )
7 df-3an 
 |-  ( ( ( n e. V /\ N e. V ) /\ n =/= N /\ E. e e. E { N , n } C_ e ) <-> ( ( ( n e. V /\ N e. V ) /\ n =/= N ) /\ E. e e. E { N , n } C_ e ) )
8 r19.42v 
 |-  ( E. e e. E ( ( ( n e. V /\ N e. V ) /\ n =/= N ) /\ { N , n } C_ e ) <-> ( ( ( n e. V /\ N e. V ) /\ n =/= N ) /\ E. e e. E { N , n } C_ e ) )
9 7 8 bitr4i 
 |-  ( ( ( n e. V /\ N e. V ) /\ n =/= N /\ E. e e. E { N , n } C_ e ) <-> E. e e. E ( ( ( n e. V /\ N e. V ) /\ n =/= N ) /\ { N , n } C_ e ) )
10 9 orbi1i 
 |-  ( ( ( ( n e. V /\ N e. V ) /\ n =/= N /\ E. e e. E { N , n } C_ e ) \/ E. e e. E ( N = n /\ e = { N } ) ) <-> ( E. e e. E ( ( ( n e. V /\ N e. V ) /\ n =/= N ) /\ { N , n } C_ e ) \/ E. e e. E ( N = n /\ e = { N } ) ) )
11 10 a1i 
 |-  ( ( N e. V /\ n e. V ) -> ( ( ( ( n e. V /\ N e. V ) /\ n =/= N /\ E. e e. E { N , n } C_ e ) \/ E. e e. E ( N = n /\ e = { N } ) ) <-> ( E. e e. E ( ( ( n e. V /\ N e. V ) /\ n =/= N ) /\ { N , n } C_ e ) \/ E. e e. E ( N = n /\ e = { N } ) ) ) )
12 r19.43 
 |-  ( E. e e. E ( ( ( ( n e. V /\ N e. V ) /\ n =/= N ) /\ { N , n } C_ e ) \/ ( N = n /\ e = { N } ) ) <-> ( E. e e. E ( ( ( n e. V /\ N e. V ) /\ n =/= N ) /\ { N , n } C_ e ) \/ E. e e. E ( N = n /\ e = { N } ) ) )
13 11 12 bitr4di 
 |-  ( ( N e. V /\ n e. V ) -> ( ( ( ( n e. V /\ N e. V ) /\ n =/= N /\ E. e e. E { N , n } C_ e ) \/ E. e e. E ( N = n /\ e = { N } ) ) <-> E. e e. E ( ( ( ( n e. V /\ N e. V ) /\ n =/= N ) /\ { N , n } C_ e ) \/ ( N = n /\ e = { N } ) ) ) )
14 6 13 bitrd 
 |-  ( ( N e. V /\ n e. V ) -> ( ( n e. ( G NeighbVtx N ) \/ E. e e. E ( N = n /\ e = { N } ) ) <-> E. e e. E ( ( ( ( n e. V /\ N e. V ) /\ n =/= N ) /\ { N , n } C_ e ) \/ ( N = n /\ e = { N } ) ) ) )
15 anass 
 |-  ( ( ( ( n e. V /\ N e. V ) /\ n =/= N ) /\ { N , n } C_ e ) <-> ( ( n e. V /\ N e. V ) /\ ( n =/= N /\ { N , n } C_ e ) ) )
16 15 a1i 
 |-  ( ( ( N e. V /\ n e. V ) /\ e e. E ) -> ( ( ( ( n e. V /\ N e. V ) /\ n =/= N ) /\ { N , n } C_ e ) <-> ( ( n e. V /\ N e. V ) /\ ( n =/= N /\ { N , n } C_ e ) ) ) )
17 ibar 
 |-  ( ( n e. V /\ N e. V ) -> ( ( n =/= N /\ { N , n } C_ e ) <-> ( ( n e. V /\ N e. V ) /\ ( n =/= N /\ { N , n } C_ e ) ) ) )
18 17 ancoms 
 |-  ( ( N e. V /\ n e. V ) -> ( ( n =/= N /\ { N , n } C_ e ) <-> ( ( n e. V /\ N e. V ) /\ ( n =/= N /\ { N , n } C_ e ) ) ) )
19 18 adantr 
 |-  ( ( ( N e. V /\ n e. V ) /\ e e. E ) -> ( ( n =/= N /\ { N , n } C_ e ) <-> ( ( n e. V /\ N e. V ) /\ ( n =/= N /\ { N , n } C_ e ) ) ) )
20 prssg 
 |-  ( ( N e. V /\ n e. V ) -> ( ( N e. e /\ n e. e ) <-> { N , n } C_ e ) )
21 20 bicomd 
 |-  ( ( N e. V /\ n e. V ) -> ( { N , n } C_ e <-> ( N e. e /\ n e. e ) ) )
22 21 adantr 
 |-  ( ( ( N e. V /\ n e. V ) /\ e e. E ) -> ( { N , n } C_ e <-> ( N e. e /\ n e. e ) ) )
23 22 anbi2d 
 |-  ( ( ( N e. V /\ n e. V ) /\ e e. E ) -> ( ( n =/= N /\ { N , n } C_ e ) <-> ( n =/= N /\ ( N e. e /\ n e. e ) ) ) )
24 3anass 
 |-  ( ( n =/= N /\ N e. e /\ n e. e ) <-> ( n =/= N /\ ( N e. e /\ n e. e ) ) )
25 23 24 bitr4di 
 |-  ( ( ( N e. V /\ n e. V ) /\ e e. E ) -> ( ( n =/= N /\ { N , n } C_ e ) <-> ( n =/= N /\ N e. e /\ n e. e ) ) )
26 16 19 25 3bitr2d 
 |-  ( ( ( N e. V /\ n e. V ) /\ e e. E ) -> ( ( ( ( n e. V /\ N e. V ) /\ n =/= N ) /\ { N , n } C_ e ) <-> ( n =/= N /\ N e. e /\ n e. e ) ) )
27 eqcom 
 |-  ( N = n <-> n = N )
28 27 anbi1i 
 |-  ( ( N = n /\ e = { N } ) <-> ( n = N /\ e = { N } ) )
29 sneq 
 |-  ( N = n -> { N } = { n } )
30 29 eqcoms 
 |-  ( n = N -> { N } = { n } )
31 30 eqeq2d 
 |-  ( n = N -> ( e = { N } <-> e = { n } ) )
32 31 pm5.32i 
 |-  ( ( n = N /\ e = { N } ) <-> ( n = N /\ e = { n } ) )
33 28 32 bitri 
 |-  ( ( N = n /\ e = { N } ) <-> ( n = N /\ e = { n } ) )
34 33 a1i 
 |-  ( ( ( N e. V /\ n e. V ) /\ e e. E ) -> ( ( N = n /\ e = { N } ) <-> ( n = N /\ e = { n } ) ) )
35 26 34 orbi12d 
 |-  ( ( ( N e. V /\ n e. V ) /\ e e. E ) -> ( ( ( ( ( n e. V /\ N e. V ) /\ n =/= N ) /\ { N , n } C_ e ) \/ ( N = n /\ e = { N } ) ) <-> ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) ) )
36 35 rexbidva 
 |-  ( ( N e. V /\ n e. V ) -> ( E. e e. E ( ( ( ( n e. V /\ N e. V ) /\ n =/= N ) /\ { N , n } C_ e ) \/ ( N = n /\ e = { N } ) ) <-> E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) ) )
37 14 36 bitrd 
 |-  ( ( N e. V /\ n e. V ) -> ( ( n e. ( G NeighbVtx N ) \/ E. e e. E ( N = n /\ e = { N } ) ) <-> E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) ) )
38 37 rabbidva 
 |-  ( N e. V -> { n e. V | ( n e. ( G NeighbVtx N ) \/ E. e e. E ( N = n /\ e = { N } ) ) } = { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } )
39 3 38 eqtrid 
 |-  ( N e. V -> U = { n e. V | E. e e. E ( ( n =/= N /\ N e. e /\ n e. e ) \/ ( n = N /\ e = { n } ) ) } )