Metamath Proof Explorer

Theorem clnbgrel

Description: Characterization of a member N of the closed neighborhood of a vertex X in a graph G . (Contributed by AV, 9-May-2025)

Ref Expression
Hypotheses clnbgrel.v 
|- V = ( Vtx ` G )
clnbgrel.e 
|- E = ( Edg ` G )
Assertion clnbgrel 
|- ( N e. ( G ClNeighbVtx X ) <-> ( ( N e. V /\ X e. V ) /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) )

Proof

Step Hyp Ref Expression
1 clnbgrel.v 
 |-  V = ( Vtx ` G )
2 clnbgrel.e 
 |-  E = ( Edg ` G )
3 1 clnbgrcl 
 |-  ( N e. ( G ClNeighbVtx X ) -> X e. V )
4 3 pm4.71ri 
 |-  ( N e. ( G ClNeighbVtx X ) <-> ( X e. V /\ N e. ( G ClNeighbVtx X ) ) )
5 1 2 clnbgrval 
 |-  ( X e. V -> ( G ClNeighbVtx X ) = ( { X } u. { n e. V | E. e e. E { X , n } C_ e } ) )
6 5 eleq2d 
 |-  ( X e. V -> ( N e. ( G ClNeighbVtx X ) <-> N e. ( { X } u. { n e. V | E. e e. E { X , n } C_ e } ) ) )
7 elun 
 |-  ( N e. ( { X } u. { n e. V | E. e e. E { X , n } C_ e } ) <-> ( N e. { X } \/ N e. { n e. V | E. e e. E { X , n } C_ e } ) )
8 elsn2g 
 |-  ( X e. V -> ( N e. { X } <-> N = X ) )
9 preq2 
 |-  ( n = N -> { X , n } = { X , N } )
10 9 sseq1d 
 |-  ( n = N -> ( { X , n } C_ e <-> { X , N } C_ e ) )
11 10 rexbidv 
 |-  ( n = N -> ( E. e e. E { X , n } C_ e <-> E. e e. E { X , N } C_ e ) )
12 11 elrab 
 |-  ( N e. { n e. V | E. e e. E { X , n } C_ e } <-> ( N e. V /\ E. e e. E { X , N } C_ e ) )
13 12 a1i 
 |-  ( X e. V -> ( N e. { n e. V | E. e e. E { X , n } C_ e } <-> ( N e. V /\ E. e e. E { X , N } C_ e ) ) )
14 8 13 orbi12d 
 |-  ( X e. V -> ( ( N e. { X } \/ N e. { n e. V | E. e e. E { X , n } C_ e } ) <-> ( N = X \/ ( N e. V /\ E. e e. E { X , N } C_ e ) ) ) )
15 7 14 bitrid 
 |-  ( X e. V -> ( N e. ( { X } u. { n e. V | E. e e. E { X , n } C_ e } ) <-> ( N = X \/ ( N e. V /\ E. e e. E { X , N } C_ e ) ) ) )
16 eleq1 
 |-  ( N = X -> ( N e. V <-> X e. V ) )
17 16 biimparc 
 |-  ( ( X e. V /\ N = X ) -> N e. V )
18 orc 
 |-  ( N = X -> ( N = X \/ E. e e. E { X , N } C_ e ) )
19 18 adantl 
 |-  ( ( X e. V /\ N = X ) -> ( N = X \/ E. e e. E { X , N } C_ e ) )
20 17 19 jca 
 |-  ( ( X e. V /\ N = X ) -> ( N e. V /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) )
21 20 ex 
 |-  ( X e. V -> ( N = X -> ( N e. V /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) ) )
22 olc 
 |-  ( E. e e. E { X , N } C_ e -> ( N = X \/ E. e e. E { X , N } C_ e ) )
23 22 anim2i 
 |-  ( ( N e. V /\ E. e e. E { X , N } C_ e ) -> ( N e. V /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) )
24 23 a1i 
 |-  ( X e. V -> ( ( N e. V /\ E. e e. E { X , N } C_ e ) -> ( N e. V /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) ) )
25 21 24 jaod 
 |-  ( X e. V -> ( ( N = X \/ ( N e. V /\ E. e e. E { X , N } C_ e ) ) -> ( N e. V /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) ) )
26 orc 
 |-  ( N = X -> ( N = X \/ ( N e. V /\ E. e e. E { X , N } C_ e ) ) )
27 26 a1i 
 |-  ( ( X e. V /\ N e. V ) -> ( N = X -> ( N = X \/ ( N e. V /\ E. e e. E { X , N } C_ e ) ) ) )
28 olc 
 |-  ( ( N e. V /\ E. e e. E { X , N } C_ e ) -> ( N = X \/ ( N e. V /\ E. e e. E { X , N } C_ e ) ) )
29 28 ex 
 |-  ( N e. V -> ( E. e e. E { X , N } C_ e -> ( N = X \/ ( N e. V /\ E. e e. E { X , N } C_ e ) ) ) )
30 29 adantl 
 |-  ( ( X e. V /\ N e. V ) -> ( E. e e. E { X , N } C_ e -> ( N = X \/ ( N e. V /\ E. e e. E { X , N } C_ e ) ) ) )
31 27 30 jaod 
 |-  ( ( X e. V /\ N e. V ) -> ( ( N = X \/ E. e e. E { X , N } C_ e ) -> ( N = X \/ ( N e. V /\ E. e e. E { X , N } C_ e ) ) ) )
32 31 expimpd 
 |-  ( X e. V -> ( ( N e. V /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) -> ( N = X \/ ( N e. V /\ E. e e. E { X , N } C_ e ) ) ) )
33 25 32 impbid 
 |-  ( X e. V -> ( ( N = X \/ ( N e. V /\ E. e e. E { X , N } C_ e ) ) <-> ( N e. V /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) ) )
34 6 15 33 3bitrd 
 |-  ( X e. V -> ( N e. ( G ClNeighbVtx X ) <-> ( N e. V /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) ) )
35 34 pm5.32i 
 |-  ( ( X e. V /\ N e. ( G ClNeighbVtx X ) ) <-> ( X e. V /\ ( N e. V /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) ) )
36 anass 
 |-  ( ( ( X e. V /\ N e. V ) /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) <-> ( X e. V /\ ( N e. V /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) ) )
37 36 bicomi 
 |-  ( ( X e. V /\ ( N e. V /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) ) <-> ( ( X e. V /\ N e. V ) /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) )
38 ancom 
 |-  ( ( X e. V /\ N e. V ) <-> ( N e. V /\ X e. V ) )
39 37 38 bianbi 
 |-  ( ( X e. V /\ ( N e. V /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) ) <-> ( ( N e. V /\ X e. V ) /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) )
40 4 35 39 3bitri 
 |-  ( N e. ( G ClNeighbVtx X ) <-> ( ( N e. V /\ X e. V ) /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) )