This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clnbgredg

Description: A vertex connected by an edge with another vertex is a neighbor of that 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 ∧ ( 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) ) → 𝑌 ∈ 𝑁 )