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 𝑋 ) ↔ ( ( 𝑁𝑉𝑋𝑉 ) ∧ 𝑁𝑋 ∧ ∃ 𝑒𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) )