Metamath Proof Explorer

Theorem clnbgredg

Description: A vertices connected by an edge with another vertex is a neigborhood of those vertex. (Contributed by AV, 24-Aug-2025)

Ref Expression
Hypotheses clnbgredg.e 
|- E = ( Edg ` G )
clnbgredg.n 
|- N = ( G ClNeighbVtx X )
Assertion clnbgredg 
|- ( ( G e. UHGraph /\ ( K e. E /\ X e. K /\ Y e. K ) ) -> Y e. N )

Proof

Step Hyp Ref Expression
1 clnbgredg.e 
 |-  E = ( Edg ` G )
2 clnbgredg.n 
 |-  N = ( G ClNeighbVtx X )
3 1 eleq2i 
 |-  ( K e. E <-> K e. ( Edg ` G ) )
4 3 biimpi 
 |-  ( K e. E -> K e. ( Edg ` G ) )
5 4 3ad2ant1 
 |-  ( ( K e. E /\ X e. K /\ Y e. K ) -> K e. ( Edg ` G ) )
6 simp3 
 |-  ( ( K e. E /\ X e. K /\ Y e. K ) -> Y e. K )
7 5 6 jca 
 |-  ( ( K e. E /\ X e. K /\ Y e. K ) -> ( K e. ( Edg ` G ) /\ Y e. K ) )
8 7 anim2i 
 |-  ( ( G e. UHGraph /\ ( K e. E /\ X e. K /\ Y e. K ) ) -> ( G e. UHGraph /\ ( K e. ( Edg ` G ) /\ Y e. K ) ) )
9 3anass 
 |-  ( ( G e. UHGraph /\ K e. ( Edg ` G ) /\ Y e. K ) <-> ( G e. UHGraph /\ ( K e. ( Edg ` G ) /\ Y e. K ) ) )
10 8 9 sylibr 
 |-  ( ( G e. UHGraph /\ ( K e. E /\ X e. K /\ Y e. K ) ) -> ( G e. UHGraph /\ K e. ( Edg ` G ) /\ Y e. K ) )
11 uhgredgrnv 
 |-  ( ( G e. UHGraph /\ K e. ( Edg ` G ) /\ Y e. K ) -> Y e. ( Vtx ` G ) )
12 10 11 syl 
 |-  ( ( G e. UHGraph /\ ( K e. E /\ X e. K /\ Y e. K ) ) -> Y e. ( Vtx ` G ) )
13 simp2 
 |-  ( ( K e. E /\ X e. K /\ Y e. K ) -> X e. K )
14 5 13 jca 
 |-  ( ( K e. E /\ X e. K /\ Y e. K ) -> ( K e. ( Edg ` G ) /\ X e. K ) )
15 14 anim2i 
 |-  ( ( G e. UHGraph /\ ( K e. E /\ X e. K /\ Y e. K ) ) -> ( G e. UHGraph /\ ( K e. ( Edg ` G ) /\ X e. K ) ) )
16 3anass 
 |-  ( ( G e. UHGraph /\ K e. ( Edg ` G ) /\ X e. K ) <-> ( G e. UHGraph /\ ( K e. ( Edg ` G ) /\ X e. K ) ) )
17 15 16 sylibr 
 |-  ( ( G e. UHGraph /\ ( K e. E /\ X e. K /\ Y e. K ) ) -> ( G e. UHGraph /\ K e. ( Edg ` G ) /\ X e. K ) )
18 uhgredgrnv 
 |-  ( ( G e. UHGraph /\ K e. ( Edg ` G ) /\ X e. K ) -> X e. ( Vtx ` G ) )
19 17 18 syl 
 |-  ( ( G e. UHGraph /\ ( K e. E /\ X e. K /\ Y e. K ) ) -> X e. ( Vtx ` G ) )
20 simpr1 
 |-  ( ( G e. UHGraph /\ ( K e. E /\ X e. K /\ Y e. K ) ) -> K e. E )
21 sseq2 
 |-  ( e = K -> ( { X , Y } C_ e <-> { X , Y } C_ K ) )
22 21 adantl 
 |-  ( ( ( G e. UHGraph /\ ( K e. E /\ X e. K /\ Y e. K ) ) /\ e = K ) -> ( { X , Y } C_ e <-> { X , Y } C_ K ) )
23 prssi 
 |-  ( ( X e. K /\ Y e. K ) -> { X , Y } C_ K )
24 23 3adant1 
 |-  ( ( K e. E /\ X e. K /\ Y e. K ) -> { X , Y } C_ K )
25 24 adantl 
 |-  ( ( G e. UHGraph /\ ( K e. E /\ X e. K /\ Y e. K ) ) -> { X , Y } C_ K )
26 20 22 25 rspcedvd 
 |-  ( ( G e. UHGraph /\ ( K e. E /\ X e. K /\ Y e. K ) ) -> E. e e. E { X , Y } C_ e )
27 26 olcd 
 |-  ( ( G e. UHGraph /\ ( K e. E /\ X e. K /\ Y e. K ) ) -> ( Y = X \/ E. e e. E { X , Y } C_ e ) )
28 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
29 28 1 clnbgrel 
 |-  ( Y e. ( G ClNeighbVtx X ) <-> ( ( Y e. ( Vtx ` G ) /\ X e. ( Vtx ` G ) ) /\ ( Y = X \/ E. e e. E { X , Y } C_ e ) ) )
30 12 19 27 29 syl21anbrc 
 |-  ( ( G e. UHGraph /\ ( K e. E /\ X e. K /\ Y e. K ) ) -> Y e. ( G ClNeighbVtx X ) )
31 2 eleq2i 
 |-  ( Y e. N <-> Y e. ( G ClNeighbVtx X ) )
32 30 31 sylibr 
 |-  ( ( G e. UHGraph /\ ( K e. E /\ X e. K /\ Y e. K ) ) -> Y e. N )