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	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	clnbgredg.n	⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑋 )
Assertion	clnbgredg	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) ) → 𝑌 ∈ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		clnbgredg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
2		clnbgredg.n	⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑋 )
3	1	eleq2i	⊢ ( 𝐾 ∈ 𝐸 ↔ 𝐾 ∈ ( Edg ‘ 𝐺 ) )
4	3	biimpi	⊢ ( 𝐾 ∈ 𝐸 → 𝐾 ∈ ( Edg ‘ 𝐺 ) )
5	4	3ad2ant1	⊢ ( ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → 𝐾 ∈ ( Edg ‘ 𝐺 ) )
6		simp3	⊢ ( ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → 𝑌 ∈ 𝐾 )
7	5 6	jca	⊢ ( ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → ( 𝐾 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐾 ) )
8	7	anim2i	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) ) → ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐾 ) ) )
9		3anass	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐾 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐾 ) ↔ ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐾 ) ) )
10	8 9	sylibr	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) ) → ( 𝐺 ∈ UHGraph ∧ 𝐾 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐾 ) )
11		uhgredgrnv	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐾 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑌 ∈ 𝐾 ) → 𝑌 ∈ ( Vtx ‘ 𝐺 ) )
12	10 11	syl	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) ) → 𝑌 ∈ ( Vtx ‘ 𝐺 ) )
13		simp2	⊢ ( ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → 𝑋 ∈ 𝐾 )
14	5 13	jca	⊢ ( ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → ( 𝐾 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑋 ∈ 𝐾 ) )
15	14	anim2i	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) ) → ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑋 ∈ 𝐾 ) ) )
16		3anass	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐾 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑋 ∈ 𝐾 ) ↔ ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑋 ∈ 𝐾 ) ) )
17	15 16	sylibr	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) ) → ( 𝐺 ∈ UHGraph ∧ 𝐾 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑋 ∈ 𝐾 ) )
18		uhgredgrnv	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐾 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑋 ∈ 𝐾 ) → 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
19	17 18	syl	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) ) → 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
20		simpr1	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) ) → 𝐾 ∈ 𝐸 )
21		sseq2	⊢ ( 𝑒 = 𝐾 → ( { 𝑋 , 𝑌 } ⊆ 𝑒 ↔ { 𝑋 , 𝑌 } ⊆ 𝐾 ) )
22	21	adantl	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) ) ∧ 𝑒 = 𝐾 ) → ( { 𝑋 , 𝑌 } ⊆ 𝑒 ↔ { 𝑋 , 𝑌 } ⊆ 𝐾 ) )
23		prssi	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → { 𝑋 , 𝑌 } ⊆ 𝐾 )
24	23	3adant1	⊢ ( ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → { 𝑋 , 𝑌 } ⊆ 𝐾 )
25	24	adantl	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) ) → { 𝑋 , 𝑌 } ⊆ 𝐾 )
26	20 22 25	rspcedvd	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) ) → ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑌 } ⊆ 𝑒 )
27	26	olcd	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) ) → ( 𝑌 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑌 } ⊆ 𝑒 ) )
28		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
29	28 1	clnbgrel	⊢ ( 𝑌 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ↔ ( ( 𝑌 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑌 = 𝑋 ∨ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑌 } ⊆ 𝑒 ) ) )
30	12 19 27 29	syl21anbrc	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) ) → 𝑌 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) )
31	2	eleq2i	⊢ ( 𝑌 ∈ 𝑁 ↔ 𝑌 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) )
32	30 31	sylibr	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) ) → 𝑌 ∈ 𝑁 )