| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | topontop 22920 | . . . . 5
⊢ (𝐾 ∈ (TopOn‘𝑋) → 𝐾 ∈ Top) | 
| 2 | 1 | ad2antrr 726 | . . . 4
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → 𝐾 ∈ Top) | 
| 3 |  | toponuni 22921 | . . . . . 6
⊢ (𝐾 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐾) | 
| 4 | 3 | ad2antrr 726 | . . . . 5
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → 𝑋 = ∪ 𝐾) | 
| 5 |  | locfincf.1 | . . . . . . 7
⊢ 𝑋 = ∪
𝐽 | 
| 6 |  | eqid 2736 | . . . . . . 7
⊢ ∪ 𝑥 =
∪ 𝑥 | 
| 7 | 5, 6 | locfinbas 23531 | . . . . . 6
⊢ (𝑥 ∈ (LocFin‘𝐽) → 𝑋 = ∪ 𝑥) | 
| 8 | 7 | adantl 481 | . . . . 5
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → 𝑋 = ∪ 𝑥) | 
| 9 | 4, 8 | eqtr3d 2778 | . . . 4
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → ∪ 𝐾 = ∪
𝑥) | 
| 10 | 4 | eleq2d 2826 | . . . . . 6
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → (𝑦 ∈ 𝑋 ↔ 𝑦 ∈ ∪ 𝐾)) | 
| 11 | 5 | locfinnei 23532 | . . . . . . . 8
⊢ ((𝑥 ∈ (LocFin‘𝐽) ∧ 𝑦 ∈ 𝑋) → ∃𝑛 ∈ 𝐽 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) | 
| 12 | 11 | ex 412 | . . . . . . 7
⊢ (𝑥 ∈ (LocFin‘𝐽) → (𝑦 ∈ 𝑋 → ∃𝑛 ∈ 𝐽 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) | 
| 13 |  | ssrexv 4052 | . . . . . . . 8
⊢ (𝐽 ⊆ 𝐾 → (∃𝑛 ∈ 𝐽 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) →
∃𝑛 ∈ 𝐾 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) | 
| 14 | 13 | adantl 481 | . . . . . . 7
⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (∃𝑛 ∈ 𝐽 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin) →
∃𝑛 ∈ 𝐾 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) | 
| 15 | 12, 14 | sylan9r 508 | . . . . . 6
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → (𝑦 ∈ 𝑋 → ∃𝑛 ∈ 𝐾 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) | 
| 16 | 10, 15 | sylbird 260 | . . . . 5
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → (𝑦 ∈ ∪ 𝐾 → ∃𝑛 ∈ 𝐾 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) | 
| 17 | 16 | ralrimiv 3144 | . . . 4
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → ∀𝑦 ∈ ∪ 𝐾∃𝑛 ∈ 𝐾 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) | 
| 18 |  | eqid 2736 | . . . . 5
⊢ ∪ 𝐾 =
∪ 𝐾 | 
| 19 | 18, 6 | islocfin 23526 | . . . 4
⊢ (𝑥 ∈ (LocFin‘𝐾) ↔ (𝐾 ∈ Top ∧ ∪ 𝐾 =
∪ 𝑥 ∧ ∀𝑦 ∈ ∪ 𝐾∃𝑛 ∈ 𝐾 (𝑦 ∈ 𝑛 ∧ {𝑠 ∈ 𝑥 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈
Fin))) | 
| 20 | 2, 9, 17, 19 | syl3anbrc 1343 | . . 3
⊢ (((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) ∧ 𝑥 ∈ (LocFin‘𝐽)) → 𝑥 ∈ (LocFin‘𝐾)) | 
| 21 | 20 | ex 412 | . 2
⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (𝑥 ∈ (LocFin‘𝐽) → 𝑥 ∈ (LocFin‘𝐾))) | 
| 22 | 21 | ssrdv 3988 | 1
⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (LocFin‘𝐽) ⊆ (LocFin‘𝐾)) |