Metamath Proof Explorer

Theorem clnbgr0edg

Description: In an empty graph (with no edges), all closed neighborhoods consists of a single vertex. (Contributed by AV, 10-May-2025)

Ref Expression
Assertion clnbgr0edg 
|- ( ( ( Edg ` G ) = (/) /\ K e. ( Vtx ` G ) ) -> ( G ClNeighbVtx K ) = { K } )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 dfclnbgr4 
 |-  ( K e. ( Vtx ` G ) -> ( G ClNeighbVtx K ) = ( { K } u. ( G NeighbVtx K ) ) )
3 2 adantl 
 |-  ( ( ( Edg ` G ) = (/) /\ K e. ( Vtx ` G ) ) -> ( G ClNeighbVtx K ) = ( { K } u. ( G NeighbVtx K ) ) )
4 nbgr0edg 
 |-  ( ( Edg ` G ) = (/) -> ( G NeighbVtx K ) = (/) )
5 4 adantr 
 |-  ( ( ( Edg ` G ) = (/) /\ K e. ( Vtx ` G ) ) -> ( G NeighbVtx K ) = (/) )
6 5 uneq2d 
 |-  ( ( ( Edg ` G ) = (/) /\ K e. ( Vtx ` G ) ) -> ( { K } u. ( G NeighbVtx K ) ) = ( { K } u. (/) ) )
7 un0 
 |-  ( { K } u. (/) ) = { K }
8 7 a1i 
 |-  ( ( ( Edg ` G ) = (/) /\ K e. ( Vtx ` G ) ) -> ( { K } u. (/) ) = { K } )
9 3 6 8 3eqtrd 
 |-  ( ( ( Edg ` G ) = (/) /\ K e. ( Vtx ` G ) ) -> ( G ClNeighbVtx K ) = { K } )