Step | Hyp | Ref
| Expression |
1 | | neifg.1 |
. . . 4
⊢ 𝑋 = ∪
𝐽 |
2 | 1 | opnfbas 22593 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∈ (fBas‘𝑋)) |
3 | | fgval 22621 |
. . 3
⊢ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∈ (fBas‘𝑋) → (𝑋filGen{𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}) = {𝑡 ∈ 𝒫 𝑋 ∣ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑡) ≠ ∅}) |
4 | 2, 3 | syl 17 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑋filGen{𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}) = {𝑡 ∈ 𝒫 𝑋 ∣ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑡) ≠ ∅}) |
5 | | pweq 4504 |
. . . . . . 7
⊢ (𝑡 = 𝑢 → 𝒫 𝑡 = 𝒫 𝑢) |
6 | 5 | ineq2d 4103 |
. . . . . 6
⊢ (𝑡 = 𝑢 → ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑡) = ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢)) |
7 | 6 | neeq1d 2993 |
. . . . 5
⊢ (𝑡 = 𝑢 → (({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑡) ≠ ∅ ↔ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ≠ ∅)) |
8 | 7 | elrab 3588 |
. . . 4
⊢ (𝑢 ∈ {𝑡 ∈ 𝒫 𝑋 ∣ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑡) ≠ ∅} ↔ (𝑢 ∈ 𝒫 𝑋 ∧ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ≠ ∅)) |
9 | | velpw 4493 |
. . . . . . 7
⊢ (𝑢 ∈ 𝒫 𝑋 ↔ 𝑢 ⊆ 𝑋) |
10 | 9 | a1i 11 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑢 ∈ 𝒫 𝑋 ↔ 𝑢 ⊆ 𝑋)) |
11 | | n0 4235 |
. . . . . . . 8
⊢ (({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢)) |
12 | | elin 3859 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ↔ (𝑧 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∧ 𝑧 ∈ 𝒫 𝑢)) |
13 | | sseq2 3903 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑧)) |
14 | 13 | elrab 3588 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ↔ (𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧)) |
15 | | velpw 4493 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝒫 𝑢 ↔ 𝑧 ⊆ 𝑢) |
16 | 14, 15 | anbi12i 630 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∧ 𝑧 ∈ 𝒫 𝑢) ↔ ((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢)) |
17 | 12, 16 | bitri 278 |
. . . . . . . . 9
⊢ (𝑧 ∈ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ↔ ((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢)) |
18 | 17 | exbii 1854 |
. . . . . . . 8
⊢
(∃𝑧 𝑧 ∈ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ↔ ∃𝑧((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢)) |
19 | 11, 18 | bitri 278 |
. . . . . . 7
⊢ (({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ≠ ∅ ↔ ∃𝑧((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢)) |
20 | 19 | a1i 11 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ≠ ∅ ↔ ∃𝑧((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢))) |
21 | 10, 20 | anbi12d 634 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ((𝑢 ∈ 𝒫 𝑋 ∧ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ≠ ∅) ↔ (𝑢 ⊆ 𝑋 ∧ ∃𝑧((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢)))) |
22 | | anass 472 |
. . . . . . . . 9
⊢ (((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢) ↔ (𝑧 ∈ 𝐽 ∧ (𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢))) |
23 | 22 | exbii 1854 |
. . . . . . . 8
⊢
(∃𝑧((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢) ↔ ∃𝑧(𝑧 ∈ 𝐽 ∧ (𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢))) |
24 | | df-rex 3059 |
. . . . . . . 8
⊢
(∃𝑧 ∈
𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢) ↔ ∃𝑧(𝑧 ∈ 𝐽 ∧ (𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢))) |
25 | 23, 24 | bitr4i 281 |
. . . . . . 7
⊢
(∃𝑧((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢) ↔ ∃𝑧 ∈ 𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢)) |
26 | 25 | anbi2i 626 |
. . . . . 6
⊢ ((𝑢 ⊆ 𝑋 ∧ ∃𝑧((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢)) ↔ (𝑢 ⊆ 𝑋 ∧ ∃𝑧 ∈ 𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢))) |
27 | 1 | isnei 21854 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑢 ∈ ((nei‘𝐽)‘𝑆) ↔ (𝑢 ⊆ 𝑋 ∧ ∃𝑧 ∈ 𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢)))) |
28 | 27 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑢 ∈ ((nei‘𝐽)‘𝑆) ↔ (𝑢 ⊆ 𝑋 ∧ ∃𝑧 ∈ 𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢)))) |
29 | 26, 28 | bitr4id 293 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ((𝑢 ⊆ 𝑋 ∧ ∃𝑧((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢)) ↔ 𝑢 ∈ ((nei‘𝐽)‘𝑆))) |
30 | 21, 29 | bitrd 282 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ((𝑢 ∈ 𝒫 𝑋 ∧ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ≠ ∅) ↔ 𝑢 ∈ ((nei‘𝐽)‘𝑆))) |
31 | 8, 30 | syl5bb 286 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑢 ∈ {𝑡 ∈ 𝒫 𝑋 ∣ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑡) ≠ ∅} ↔ 𝑢 ∈ ((nei‘𝐽)‘𝑆))) |
32 | 31 | eqrdv 2736 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → {𝑡 ∈ 𝒫 𝑋 ∣ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑡) ≠ ∅} = ((nei‘𝐽)‘𝑆)) |
33 | 4, 32 | eqtrd 2773 |
1
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑋filGen{𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}) = ((nei‘𝐽)‘𝑆)) |