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

Metamath Proof Explorer

Theorem nbgrel

Description: Characterization of a neighbor N of a vertex X in a graph G . (Contributed by Alexander van der Vekens and Mario Carneiro, 9-Oct-2017) (Revised by AV, 26-Oct-2020) (Revised by AV, 12-Feb-2022)

Ref Expression
Hypotheses nbgrel.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
nbgrel.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion nbgrel ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )

Proof

Step Hyp Ref Expression
1 nbgrel.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 nbgrel.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 nbgrcl ⊢ ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) → 𝑋 ∈ 𝑉 )
4 3 pm4.71ri ⊢ ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) )
5 1 2 nbgrval ⊢ ( 𝑋 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑋 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑋 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 } )
6 5 eleq2d ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ 𝑁 ∈ { 𝑛 ∈ ( 𝑉 ∖ { 𝑋 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 } ) )
7 preq2 ⊢ ( 𝑛 = 𝑁 → { 𝑋 , 𝑛 } = { 𝑋 , 𝑁 } )
8 7 sseq1d ⊢ ( 𝑛 = 𝑁 → ( { 𝑋 , 𝑛 } ⊆ 𝑒 ↔ { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
9 8 rexbidv ⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
10 9 elrab ⊢ ( 𝑁 ∈ { 𝑛 ∈ ( 𝑉 ∖ { 𝑋 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 } ↔ ( 𝑁 ∈ ( 𝑉 ∖ { 𝑋 } ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
11 eldifsn ⊢ ( 𝑁 ∈ ( 𝑉 ∖ { 𝑋 } ) ↔ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) )
12 11 anbi1i ⊢ ( ( 𝑁 ∈ ( 𝑉 ∖ { 𝑋 } ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
13 10 12 bitri ⊢ ( 𝑁 ∈ { 𝑛 ∈ ( 𝑉 ∖ { 𝑋 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑛 } ⊆ 𝑒 } ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
14 6 13 bitrdi ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) )
15 14 pm5.32i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ↔ ( 𝑋 ∈ 𝑉 ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) )
16 df-3an ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ↔ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
17 anass ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ) ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ) )
18 ancom ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ↔ ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) )
19 18 anbi1i ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ) )
20 17 19 bitr3i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ) )
21 20 anbi1i ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ↔ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
22 anass ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ↔ ( 𝑋 ∈ 𝑉 ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) )
23 16 21 22 3bitr2ri ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝑋 ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
24 15 23 bitri ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )
25 4 24 bitri ⊢ ( 𝑁 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )