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 𝐾 ) ↔ ( 𝑁 = 𝐾 ∨ { 𝑁 , 𝐾 } ∈ 𝐸 ) ) )