| Step | Hyp | Ref
| Expression |
| 1 | | toponuni 22920 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
| 2 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝑋 = ∪ 𝐽) |
| 3 | | topontop 22919 |
. . . . . . . . 9
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
| 4 | 3 | adantr 480 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐽 ∈ Top) |
| 5 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ 𝑋) |
| 6 | 5, 2 | sseqtrd 4020 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ ∪ 𝐽) |
| 7 | | eqid 2737 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 8 | 7 | neiuni 23130 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ ∪ 𝐽 = ∪
((nei‘𝐽)‘𝑆)) |
| 9 | 4, 6, 8 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → ∪ 𝐽 = ∪
((nei‘𝐽)‘𝑆)) |
| 10 | 2, 9 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝑋 = ∪
((nei‘𝐽)‘𝑆)) |
| 11 | | eqimss2 4043 |
. . . . . 6
⊢ (𝑋 = ∪
((nei‘𝐽)‘𝑆) → ∪ ((nei‘𝐽)‘𝑆) ⊆ 𝑋) |
| 12 | 10, 11 | syl 17 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → ∪
((nei‘𝐽)‘𝑆) ⊆ 𝑋) |
| 13 | | sspwuni 5100 |
. . . . 5
⊢
(((nei‘𝐽)‘𝑆) ⊆ 𝒫 𝑋 ↔ ∪
((nei‘𝐽)‘𝑆) ⊆ 𝑋) |
| 14 | 12, 13 | sylibr 234 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → ((nei‘𝐽)‘𝑆) ⊆ 𝒫 𝑋) |
| 15 | 14 | 3adant3 1133 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ((nei‘𝐽)‘𝑆) ⊆ 𝒫 𝑋) |
| 16 | | 0nnei 23120 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ≠ ∅) → ¬
∅ ∈ ((nei‘𝐽)‘𝑆)) |
| 17 | 3, 16 | sylan 580 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ≠ ∅) → ¬ ∅ ∈
((nei‘𝐽)‘𝑆)) |
| 18 | 17 | 3adant2 1132 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ¬ ∅ ∈
((nei‘𝐽)‘𝑆)) |
| 19 | 7 | tpnei 23129 |
. . . . . . 7
⊢ (𝐽 ∈ Top → (𝑆 ⊆ ∪ 𝐽
↔ ∪ 𝐽 ∈ ((nei‘𝐽)‘𝑆))) |
| 20 | 19 | biimpa 476 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ ∪ 𝐽 ∈ ((nei‘𝐽)‘𝑆)) |
| 21 | 4, 6, 20 | syl2anc 584 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → ∪ 𝐽 ∈ ((nei‘𝐽)‘𝑆)) |
| 22 | 2, 21 | eqeltrd 2841 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝑋 ∈ ((nei‘𝐽)‘𝑆)) |
| 23 | 22 | 3adant3 1133 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → 𝑋 ∈ ((nei‘𝐽)‘𝑆)) |
| 24 | 15, 18, 23 | 3jca 1129 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (((nei‘𝐽)‘𝑆) ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
((nei‘𝐽)‘𝑆) ∧ 𝑋 ∈ ((nei‘𝐽)‘𝑆))) |
| 25 | | elpwi 4607 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋) |
| 26 | 4 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ (𝑦 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑦 ⊆ 𝑥)) → 𝐽 ∈ Top) |
| 27 | | simprl 771 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ (𝑦 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ∈ ((nei‘𝐽)‘𝑆)) |
| 28 | | simprr 773 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ (𝑦 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ⊆ 𝑥) |
| 29 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ (𝑦 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑦 ⊆ 𝑥)) → 𝑥 ⊆ 𝑋) |
| 30 | 2 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ (𝑦 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑦 ⊆ 𝑥)) → 𝑋 = ∪ 𝐽) |
| 31 | 29, 30 | sseqtrd 4020 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ (𝑦 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑦 ⊆ 𝑥)) → 𝑥 ⊆ ∪ 𝐽) |
| 32 | 7 | ssnei2 23124 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑦 ∈ ((nei‘𝐽)‘𝑆)) ∧ (𝑦 ⊆ 𝑥 ∧ 𝑥 ⊆ ∪ 𝐽)) → 𝑥 ∈ ((nei‘𝐽)‘𝑆)) |
| 33 | 26, 27, 28, 31, 32 | syl22anc 839 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑋) ∧ (𝑦 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ ((nei‘𝐽)‘𝑆)) |
| 34 | 33 | rexlimdvaa 3156 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑋) → (∃𝑦 ∈ ((nei‘𝐽)‘𝑆)𝑦 ⊆ 𝑥 → 𝑥 ∈ ((nei‘𝐽)‘𝑆))) |
| 35 | 25, 34 | sylan2 593 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ 𝒫 𝑋) → (∃𝑦 ∈ ((nei‘𝐽)‘𝑆)𝑦 ⊆ 𝑥 → 𝑥 ∈ ((nei‘𝐽)‘𝑆))) |
| 36 | 35 | ralrimiva 3146 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ ((nei‘𝐽)‘𝑆)𝑦 ⊆ 𝑥 → 𝑥 ∈ ((nei‘𝐽)‘𝑆))) |
| 37 | 36 | 3adant3 1133 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ ((nei‘𝐽)‘𝑆)𝑦 ⊆ 𝑥 → 𝑥 ∈ ((nei‘𝐽)‘𝑆))) |
| 38 | | innei 23133 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((nei‘𝐽)‘𝑆)) → (𝑥 ∩ 𝑦) ∈ ((nei‘𝐽)‘𝑆)) |
| 39 | 38 | 3expib 1123 |
. . . . 5
⊢ (𝐽 ∈ Top → ((𝑥 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((nei‘𝐽)‘𝑆)) → (𝑥 ∩ 𝑦) ∈ ((nei‘𝐽)‘𝑆))) |
| 40 | 3, 39 | syl 17 |
. . . 4
⊢ (𝐽 ∈ (TopOn‘𝑋) → ((𝑥 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((nei‘𝐽)‘𝑆)) → (𝑥 ∩ 𝑦) ∈ ((nei‘𝐽)‘𝑆))) |
| 41 | 40 | 3ad2ant1 1134 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ((𝑥 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑦 ∈ ((nei‘𝐽)‘𝑆)) → (𝑥 ∩ 𝑦) ∈ ((nei‘𝐽)‘𝑆))) |
| 42 | 41 | ralrimivv 3200 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ∀𝑥 ∈ ((nei‘𝐽)‘𝑆)∀𝑦 ∈ ((nei‘𝐽)‘𝑆)(𝑥 ∩ 𝑦) ∈ ((nei‘𝐽)‘𝑆)) |
| 43 | | isfil2 23864 |
. 2
⊢
(((nei‘𝐽)‘𝑆) ∈ (Fil‘𝑋) ↔ ((((nei‘𝐽)‘𝑆) ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
((nei‘𝐽)‘𝑆) ∧ 𝑋 ∈ ((nei‘𝐽)‘𝑆)) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ ((nei‘𝐽)‘𝑆)𝑦 ⊆ 𝑥 → 𝑥 ∈ ((nei‘𝐽)‘𝑆)) ∧ ∀𝑥 ∈ ((nei‘𝐽)‘𝑆)∀𝑦 ∈ ((nei‘𝐽)‘𝑆)(𝑥 ∩ 𝑦) ∈ ((nei‘𝐽)‘𝑆))) |
| 44 | 24, 37, 42, 43 | syl3anbrc 1344 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ((nei‘𝐽)‘𝑆) ∈ (Fil‘𝑋)) |