Step | Hyp | Ref
| Expression |
1 | | simplll 794 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ 𝐽 ⊆ 𝐾) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ (𝐾 fLim 𝑓))) → 𝐽 ∈ (TopOn‘𝑋)) |
2 | | simprl 790 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ 𝐽 ⊆ 𝐾) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ (𝐾 fLim 𝑓))) → 𝑓 ∈ (Fil‘𝑋)) |
3 | | simplr 788 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ 𝐽 ⊆ 𝐾) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ (𝐾 fLim 𝑓))) → 𝐽 ⊆ 𝐾) |
4 | | flimss1 21587 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) |
5 | 1, 2, 3, 4 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ 𝐽 ⊆ 𝐾) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ (𝐾 fLim 𝑓))) → (𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) |
6 | | simprr 792 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ 𝐽 ⊆ 𝐾) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ (𝐾 fLim 𝑓))) → 𝑥 ∈ (𝐾 fLim 𝑓)) |
7 | 5, 6 | sseldd 3569 |
. . . . 5
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ 𝐽 ⊆ 𝐾) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ (𝐾 fLim 𝑓))) → 𝑥 ∈ (𝐽 fLim 𝑓)) |
8 | 7 | expr 641 |
. . . 4
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑓 ∈ (Fil‘𝑋)) → (𝑥 ∈ (𝐾 fLim 𝑓) → 𝑥 ∈ (𝐽 fLim 𝑓))) |
9 | 8 | ssrdv 3574 |
. . 3
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑓 ∈ (Fil‘𝑋)) → (𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) |
10 | 9 | ralrimiva 2949 |
. 2
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ 𝐽 ⊆ 𝐾) → ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) |
11 | | simpllr 795 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝐾 ∈ (TopOn‘𝑋)) |
12 | | simplll 794 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝐽 ∈ (TopOn‘𝑋)) |
13 | | simprl 790 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ∈ 𝐽) |
14 | | toponss 20544 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ∈ 𝐽) → 𝑥 ⊆ 𝑋) |
15 | 12, 13, 14 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ⊆ 𝑋) |
16 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ 𝑥) |
17 | 15, 16 | sseldd 3569 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ 𝑋) |
18 | 17 | snssd 4281 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → {𝑦} ⊆ 𝑋) |
19 | | snnzg 4251 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑋 → {𝑦} ≠ ∅) |
20 | 17, 19 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → {𝑦} ≠ ∅) |
21 | | neifil 21494 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ {𝑦} ⊆ 𝑋 ∧ {𝑦} ≠ ∅) → ((nei‘𝐾)‘{𝑦}) ∈ (Fil‘𝑋)) |
22 | 11, 18, 20, 21 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ((nei‘𝐾)‘{𝑦}) ∈ (Fil‘𝑋)) |
23 | | simplr 788 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) |
24 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑓 = ((nei‘𝐾)‘{𝑦}) → (𝐾 fLim 𝑓) = (𝐾 fLim ((nei‘𝐾)‘{𝑦}))) |
25 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑓 = ((nei‘𝐾)‘{𝑦}) → (𝐽 fLim 𝑓) = (𝐽 fLim ((nei‘𝐾)‘{𝑦}))) |
26 | 24, 25 | sseq12d 3597 |
. . . . . . . . . . . 12
⊢ (𝑓 = ((nei‘𝐾)‘{𝑦}) → ((𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓) ↔ (𝐾 fLim ((nei‘𝐾)‘{𝑦})) ⊆ (𝐽 fLim ((nei‘𝐾)‘{𝑦})))) |
27 | 26 | rspcv 3278 |
. . . . . . . . . . 11
⊢
(((nei‘𝐾)‘{𝑦}) ∈ (Fil‘𝑋) → (∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓) → (𝐾 fLim ((nei‘𝐾)‘{𝑦})) ⊆ (𝐽 fLim ((nei‘𝐾)‘{𝑦})))) |
28 | 22, 23, 27 | sylc 63 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → (𝐾 fLim ((nei‘𝐾)‘{𝑦})) ⊆ (𝐽 fLim ((nei‘𝐾)‘{𝑦}))) |
29 | | neiflim 21588 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ (𝐾 fLim ((nei‘𝐾)‘{𝑦}))) |
30 | 11, 17, 29 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ (𝐾 fLim ((nei‘𝐾)‘{𝑦}))) |
31 | 28, 30 | sseldd 3569 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ (𝐽 fLim ((nei‘𝐾)‘{𝑦}))) |
32 | | flimneiss 21580 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝐽 fLim ((nei‘𝐾)‘{𝑦})) → ((nei‘𝐽)‘{𝑦}) ⊆ ((nei‘𝐾)‘{𝑦})) |
33 | 31, 32 | syl 17 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → ((nei‘𝐽)‘{𝑦}) ⊆ ((nei‘𝐾)‘{𝑦})) |
34 | | topontop 20541 |
. . . . . . . . . 10
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
35 | 12, 34 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝐽 ∈ Top) |
36 | | opnneip 20733 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ ((nei‘𝐽)‘{𝑦})) |
37 | 35, 13, 16, 36 | syl3anc 1318 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ∈ ((nei‘𝐽)‘{𝑦})) |
38 | 33, 37 | sseldd 3569 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ∈ ((nei‘𝐾)‘{𝑦})) |
39 | 38 | anassrs 678 |
. . . . . 6
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ ((nei‘𝐾)‘{𝑦})) |
40 | 39 | ralrimiva 2949 |
. . . . 5
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ 𝑥 ∈ 𝐽) → ∀𝑦 ∈ 𝑥 𝑥 ∈ ((nei‘𝐾)‘{𝑦})) |
41 | | simpllr 795 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ 𝑥 ∈ 𝐽) → 𝐾 ∈ (TopOn‘𝑋)) |
42 | | topontop 20541 |
. . . . . 6
⊢ (𝐾 ∈ (TopOn‘𝑋) → 𝐾 ∈ Top) |
43 | | opnnei 20734 |
. . . . . 6
⊢ (𝐾 ∈ Top → (𝑥 ∈ 𝐾 ↔ ∀𝑦 ∈ 𝑥 𝑥 ∈ ((nei‘𝐾)‘{𝑦}))) |
44 | 41, 42, 43 | 3syl 18 |
. . . . 5
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ 𝑥 ∈ 𝐽) → (𝑥 ∈ 𝐾 ↔ ∀𝑦 ∈ 𝑥 𝑥 ∈ ((nei‘𝐾)‘{𝑦}))) |
45 | 40, 44 | mpbird 246 |
. . . 4
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ 𝐾) |
46 | 45 | ex 449 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) → (𝑥 ∈ 𝐽 → 𝑥 ∈ 𝐾)) |
47 | 46 | ssrdv 3574 |
. 2
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)) → 𝐽 ⊆ 𝐾) |
48 | 10, 47 | impbida 873 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) → (𝐽 ⊆ 𝐾 ↔ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓))) |