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 Could not format assertion : No typesetting found for |- ( N e. ( G ClNeighbVtx X ) <-> ( ( N e. V /\ X e. V ) /\ ( N = X \/ E. e e. E { X , N } C_ e ) ) ) with typecode |-

Proof

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