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 UHGraph K E X K Y K Y N

Proof

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