This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clnbupgrel

Description: A member of the closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025)

Ref Expression
Hypotheses clnbuhgr.v 
|- V = ( Vtx ` G )
clnbuhgr.e 
|- E = ( Edg ` G )
Assertion clnbupgrel 
|- ( ( G e. UPGraph /\ K e. V /\ N e. V ) -> ( N e. ( G ClNeighbVtx K ) <-> ( N = K \/ { N , K } e. E ) ) )

Proof

Step Hyp Ref Expression
1 clnbuhgr.v 
 |-  V = ( Vtx ` G )
2 clnbuhgr.e 
 |-  E = ( Edg ` G )
3 1 2 clnbupgr 
 |-  ( ( G e. UPGraph /\ K e. V ) -> ( G ClNeighbVtx K ) = ( { K } u. { n e. V | { K , n } e. E } ) )
4 3 eleq2d 
 |-  ( ( G e. UPGraph /\ K e. V ) -> ( N e. ( G ClNeighbVtx K ) <-> N e. ( { K } u. { n e. V | { K , n } e. E } ) ) )
5 4 3adant3 
 |-  ( ( G e. UPGraph /\ K e. V /\ N e. V ) -> ( N e. ( G ClNeighbVtx K ) <-> N e. ( { K } u. { n e. V | { K , n } e. E } ) ) )
6 elun 
 |-  ( N e. ( { K } u. { n e. V | { K , n } e. E } ) <-> ( N e. { K } \/ N e. { n e. V | { K , n } e. E } ) )
7 preq2 
 |-  ( n = N -> { K , n } = { K , N } )
8 7 eleq1d 
 |-  ( n = N -> ( { K , n } e. E <-> { K , N } e. E ) )
9 8 elrab 
 |-  ( N e. { n e. V | { K , n } e. E } <-> ( N e. V /\ { K , N } e. E ) )
10 9 orbi2i 
 |-  ( ( N e. { K } \/ N e. { n e. V | { K , n } e. E } ) <-> ( N e. { K } \/ ( N e. V /\ { K , N } e. E ) ) )
11 6 10 bitri 
 |-  ( N e. ( { K } u. { n e. V | { K , n } e. E } ) <-> ( N e. { K } \/ ( N e. V /\ { K , N } e. E ) ) )
12 elsng 
 |-  ( N e. V -> ( N e. { K } <-> N = K ) )
13 12 3ad2ant3 
 |-  ( ( G e. UPGraph /\ K e. V /\ N e. V ) -> ( N e. { K } <-> N = K ) )
14 13 orbi1d 
 |-  ( ( G e. UPGraph /\ K e. V /\ N e. V ) -> ( ( N e. { K } \/ ( N e. V /\ { K , N } e. E ) ) <-> ( N = K \/ ( N e. V /\ { K , N } e. E ) ) ) )
15 11 14 bitrid 
 |-  ( ( G e. UPGraph /\ K e. V /\ N e. V ) -> ( N e. ( { K } u. { n e. V | { K , n } e. E } ) <-> ( N = K \/ ( N e. V /\ { K , N } e. E ) ) ) )
16 ibar 
 |-  ( N e. V -> ( { K , N } e. E <-> ( N e. V /\ { K , N } e. E ) ) )
17 prcom 
 |-  { K , N } = { N , K }
18 17 eleq1i 
 |-  ( { K , N } e. E <-> { N , K } e. E )
19 16 18 bitr3di 
 |-  ( N e. V -> ( ( N e. V /\ { K , N } e. E ) <-> { N , K } e. E ) )
20 19 orbi2d 
 |-  ( N e. V -> ( ( N = K \/ ( N e. V /\ { K , N } e. E ) ) <-> ( N = K \/ { N , K } e. E ) ) )
21 20 3ad2ant3 
 |-  ( ( G e. UPGraph /\ K e. V /\ N e. V ) -> ( ( N = K \/ ( N e. V /\ { K , N } e. E ) ) <-> ( N = K \/ { N , K } e. E ) ) )
22 5 15 21 3bitrd 
 |-  ( ( G e. UPGraph /\ K e. V /\ N e. V ) -> ( N e. ( G ClNeighbVtx K ) <-> ( N = K \/ { N , K } e. E ) ) )