Metamath Proof Explorer

Theorem clnbupgrel

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

Ref Expression
Hypotheses clnbuhgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
clnbuhgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion clnbupgrel ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ↔ ( 𝑁 = 𝐾 ∨ { 𝑁 , 𝐾 } ∈ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 clnbuhgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 clnbuhgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 clnbupgr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) → ( 𝐺 ClNeighbVtx 𝐾 ) = ( { 𝐾 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) )
4 3 eleq2d ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) → ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ↔ 𝑁 ∈ ( { 𝐾 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) ) )
5 4 3adant3 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ↔ 𝑁 ∈ ( { 𝐾 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) ) )
6 elun ⊢ ( 𝑁 ∈ ( { 𝐾 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) ↔ ( 𝑁 ∈ { 𝐾 } ∨ 𝑁 ∈ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) )
7 preq2 ⊢ ( 𝑛 = 𝑁 → { 𝐾 , 𝑛 } = { 𝐾 , 𝑁 } )
8 7 eleq1d ⊢ ( 𝑛 = 𝑁 → ( { 𝐾 , 𝑛 } ∈ 𝐸 ↔ { 𝐾 , 𝑁 } ∈ 𝐸 ) )
9 8 elrab ⊢ ( 𝑁 ∈ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ↔ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) )
10 9 orbi2i ⊢ ( ( 𝑁 ∈ { 𝐾 } ∨ 𝑁 ∈ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) ↔ ( 𝑁 ∈ { 𝐾 } ∨ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) )
11 6 10 bitri ⊢ ( 𝑁 ∈ ( { 𝐾 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) ↔ ( 𝑁 ∈ { 𝐾 } ∨ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) )
12 elsng ⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∈ { 𝐾 } ↔ 𝑁 = 𝐾 ) )
13 12 3ad2ant3 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∈ { 𝐾 } ↔ 𝑁 = 𝐾 ) )
14 13 orbi1d ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑁 ∈ { 𝐾 } ∨ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) ↔ ( 𝑁 = 𝐾 ∨ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) ) )
15 11 14 bitrid ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∈ ( { 𝐾 } ∪ { 𝑛 ∈ 𝑉 ∣ { 𝐾 , 𝑛 } ∈ 𝐸 } ) ↔ ( 𝑁 = 𝐾 ∨ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) ) )
16 ibar ⊢ ( 𝑁 ∈ 𝑉 → ( { 𝐾 , 𝑁 } ∈ 𝐸 ↔ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) )
17 prcom ⊢ { 𝐾 , 𝑁 } = { 𝑁 , 𝐾 }
18 17 eleq1i ⊢ ( { 𝐾 , 𝑁 } ∈ 𝐸 ↔ { 𝑁 , 𝐾 } ∈ 𝐸 )
19 16 18 bitr3di ⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ↔ { 𝑁 , 𝐾 } ∈ 𝐸 ) )
20 19 orbi2d ⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑁 = 𝐾 ∨ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) ↔ ( 𝑁 = 𝐾 ∨ { 𝑁 , 𝐾 } ∈ 𝐸 ) ) )
21 20 3ad2ant3 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑁 = 𝐾 ∨ ( 𝑁 ∈ 𝑉 ∧ { 𝐾 , 𝑁 } ∈ 𝐸 ) ) ↔ ( 𝑁 = 𝐾 ∨ { 𝑁 , 𝐾 } ∈ 𝐸 ) ) )
22 5 15 21 3bitrd ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑁 ∈ ( 𝐺 ClNeighbVtx 𝐾 ) ↔ ( 𝑁 = 𝐾 ∨ { 𝑁 , 𝐾 } ∈ 𝐸 ) ) )