Metamath Proof Explorer

Theorem clnbupgreli

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

Ref Expression
Hypothesis clnbupgreli.e 
|- E = ( Edg ` G )
Assertion clnbupgreli 
|- ( ( G e. UPGraph /\ N e. ( G ClNeighbVtx K ) ) -> ( N = K \/ { N , K } e. E ) )

Proof

Step Hyp Ref Expression
1 clnbupgreli.e 
 |-  E = ( Edg ` G )
2 simpr 
 |-  ( ( G e. UPGraph /\ N e. ( G ClNeighbVtx K ) ) -> N e. ( G ClNeighbVtx K ) )
3 simpl 
 |-  ( ( G e. UPGraph /\ N e. ( G ClNeighbVtx K ) ) -> G e. UPGraph )
4 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
5 4 clnbgrcl 
 |-  ( N e. ( G ClNeighbVtx K ) -> K e. ( Vtx ` G ) )
6 5 adantl 
 |-  ( ( G e. UPGraph /\ N e. ( G ClNeighbVtx K ) ) -> K e. ( Vtx ` G ) )
7 4 clnbgrisvtx 
 |-  ( N e. ( G ClNeighbVtx K ) -> N e. ( Vtx ` G ) )
8 7 adantl 
 |-  ( ( G e. UPGraph /\ N e. ( G ClNeighbVtx K ) ) -> N e. ( Vtx ` G ) )
9 4 1 clnbupgrel 
 |-  ( ( G e. UPGraph /\ K e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) -> ( N e. ( G ClNeighbVtx K ) <-> ( N = K \/ { N , K } e. E ) ) )
10 3 6 8 9 syl3anc 
 |-  ( ( G e. UPGraph /\ N e. ( G ClNeighbVtx K ) ) -> ( N e. ( G ClNeighbVtx K ) <-> ( N = K \/ { N , K } e. E ) ) )
11 2 10 mpbid 
 |-  ( ( G e. UPGraph /\ N e. ( G ClNeighbVtx K ) ) -> ( N = K \/ { N , K } e. E ) )