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
|
syl6bb |
⊢ ( 𝑋 ∈ 𝑉 → ( 𝑁 ∈ ( 𝐺 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 𝑋 ) ↔ ( ( 𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 ≠ 𝑋 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑋 , 𝑁 } ⊆ 𝑒 ) ) |