Step |
Hyp |
Ref |
Expression |
1 |
|
neifval.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
snssi |
⊢ ( 𝑃 ∈ 𝑋 → { 𝑃 } ⊆ 𝑋 ) |
3 |
1
|
isnei |
⊢ ( ( 𝐽 ∈ Top ∧ { 𝑃 } ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) ) |
4 |
2 3
|
sylan2 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) ) |
5 |
|
snssg |
⊢ ( 𝑃 ∈ 𝑋 → ( 𝑃 ∈ 𝑔 ↔ { 𝑃 } ⊆ 𝑔 ) ) |
6 |
5
|
anbi1d |
⊢ ( 𝑃 ∈ 𝑋 → ( ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ↔ ( { 𝑃 } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) |
7 |
6
|
rexbidv |
⊢ ( 𝑃 ∈ 𝑋 → ( ∃ 𝑔 ∈ 𝐽 ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ↔ ∃ 𝑔 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) |
8 |
7
|
anbi2d |
⊢ ( 𝑃 ∈ 𝑋 → ( ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) ) |
9 |
8
|
adantl |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( { 𝑃 } ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) ) |
10 |
4 9
|
bitr4d |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁 ) ) ) ) |