Step | Hyp | Ref
| Expression |
1 | | topontop 21515 |
. . . . 5
⊢ (𝐾 ∈ (TopOn‘𝑋) → 𝐾 ∈ Top) |
2 | 1 | ad2antrr 724 |
. . . 4
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → 𝐾 ∈ Top) |
3 | | toponuni 21516 |
. . . . . 6
⊢ (𝐾 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐾) |
4 | 3 | ad2antrr 724 |
. . . . 5
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → 𝑋 = ∪ 𝐾) |
5 | | locfincf.1 |
. . . . . . 7
⊢ 𝑋 = ∪
𝐽 |
6 | | eqid 2821 |
. . . . . . 7
⊢ ∪ 𝑥 =
∪ 𝑥 |
7 | 5, 6 | locfinbas 22124 |
. . . . . 6
⊢ (𝑥 ∈ (LocFin‘𝐽) → 𝑋 = ∪ 𝑥) |
8 | 7 | adantl 484 |
. . . . 5
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → 𝑋 = ∪ 𝑥) |
9 | 4, 8 | eqtr3d 2858 |
. . . 4
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → ∪ 𝐾 = ∪
𝑥) |
10 | 4 | eleq2d 2898 |
. . . . . 6
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → (𝑦 ∈ 𝑋 ↔ 𝑦 ∈ ∪ 𝐾)) |
11 | 5 | locfinnei 22125 |
. . . . . . . 8
⊢ ((𝑥 ∈ (LocFin‘𝐽) ∧ 𝑦 ∈ 𝑋) → ∃𝑛 ∈ 𝐽 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
12 | 11 | ex 415 |
. . . . . . 7
⊢ (𝑥 ∈ (LocFin‘𝐽) → (𝑦 ∈ 𝑋 → ∃𝑛 ∈ 𝐽 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
13 | | ssrexv 4033 |
. . . . . . . 8
⊢ (𝐽 ⊆ 𝐾 → (∃𝑛 ∈ 𝐽 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) →
∃𝑛 ∈ 𝐾 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
14 | 13 | adantl 484 |
. . . . . . 7
⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (∃𝑛 ∈ 𝐽 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) →
∃𝑛 ∈ 𝐾 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
15 | 12, 14 | sylan9r 511 |
. . . . . 6
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → (𝑦 ∈ 𝑋 → ∃𝑛 ∈ 𝐾 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
16 | 10, 15 | sylbird 262 |
. . . . 5
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → (𝑦 ∈ ∪ 𝐾 → ∃𝑛 ∈ 𝐾 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
17 | 16 | ralrimiv 3181 |
. . . 4
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → ∀𝑦 ∈ ∪ 𝐾∃𝑛 ∈ 𝐾 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) |
18 | | eqid 2821 |
. . . . 5
⊢ ∪ 𝐾 =
∪ 𝐾 |
19 | 18, 6 | islocfin 22119 |
. . . 4
⊢ (𝑥 ∈ (LocFin‘𝐾) ↔ (𝐾 ∈ Top ∧ ∪ 𝐾 =
∪ 𝑥 ∧ ∀𝑦 ∈ ∪ 𝐾∃𝑛 ∈ 𝐾 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) |
20 | 2, 9, 17, 19 | syl3anbrc 1339 |
. . 3
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → 𝑥 ∈ (LocFin‘𝐾)) |
21 | 20 | ex 415 |
. 2
⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (𝑥 ∈ (LocFin‘𝐽) → 𝑥 ∈ (LocFin‘𝐾))) |
22 | 21 | ssrdv 3972 |
1
⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (LocFin‘𝐽) ⊆ (LocFin‘𝐾)) |