Metamath Proof Explorer

Theorem dfclnbgr4

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

Ref Expression
Hypothesis dfclnbgr4.v ⊢ V = Vtx ⁡ G
Assertion dfclnbgr4 Could not format assertion : No typesetting found for |- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. ( G NeighbVtx N ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 dfclnbgr4.v ⊢ V = Vtx ⁡ G
2 eqid ⊢ Edg ⁡ G = Edg ⁡ G
3 1 2 dfclnbgr2 Could not format ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. ( Edg ` G ) ( N e. e /\ n e. e ) } ) ) : No typesetting found for |- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. ( Edg ` G ) ( N e. e /\ n e. e ) } ) ) with typecode |-
4 undif2 ⊢ N ∪ n ∈ V | ∃ e ∈ Edg ⁡ G N ∈ e ∧ n ∈ e ∖ N = N ∪ n ∈ V | ∃ e ∈ Edg ⁡ G N ∈ e ∧ n ∈ e
5 rabdif ⊢ n ∈ V | ∃ e ∈ Edg ⁡ G N ∈ e ∧ n ∈ e ∖ N = n ∈ V ∖ N | ∃ e ∈ Edg ⁡ G N ∈ e ∧ n ∈ e
6 5 uneq2i ⊢ N ∪ n ∈ V | ∃ e ∈ Edg ⁡ G N ∈ e ∧ n ∈ e ∖ N = N ∪ n ∈ V ∖ N | ∃ e ∈ Edg ⁡ G N ∈ e ∧ n ∈ e
7 4 6 eqtr3i ⊢ N ∪ n ∈ V | ∃ e ∈ Edg ⁡ G N ∈ e ∧ n ∈ e = N ∪ n ∈ V ∖ N | ∃ e ∈ Edg ⁡ G N ∈ e ∧ n ∈ e
8 1 2 dfnbgr2 ⊢ N ∈ V → G NeighbVtx N = n ∈ V ∖ N | ∃ e ∈ Edg ⁡ G N ∈ e ∧ n ∈ e
9 8 eqcomd ⊢ N ∈ V → n ∈ V ∖ N | ∃ e ∈ Edg ⁡ G N ∈ e ∧ n ∈ e = G NeighbVtx N
10 9 uneq2d ⊢ N ∈ V → N ∪ n ∈ V ∖ N | ∃ e ∈ Edg ⁡ G N ∈ e ∧ n ∈ e = N ∪ G NeighbVtx N
11 7 10 eqtrid ⊢ N ∈ V → N ∪ n ∈ V | ∃ e ∈ Edg ⁡ G N ∈ e ∧ n ∈ e = N ∪ G NeighbVtx N
12 3 11 eqtrd Could not format ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. ( G NeighbVtx N ) ) ) : No typesetting found for |- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. ( G NeighbVtx N ) ) ) with typecode |-