Step | Hyp | Ref
| Expression |
1 | | cmptop 21008 |
. 2
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
2 | | cmpcref 29245 |
. . . . . 6
⊢ Comp =
CovHasRefFin |
3 | 2 | eleq2i 2680 |
. . . . 5
⊢ (𝐽 ∈ Comp ↔ 𝐽 ∈
CovHasRefFin) |
4 | | eqid 2610 |
. . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 |
5 | 4 | iscref 29239 |
. . . . 5
⊢ (𝐽 ∈ CovHasRefFin ↔
(𝐽 ∈ Top ∧
∀𝑦 ∈ 𝒫
𝐽(∪ 𝐽 =
∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)𝑧Ref𝑦))) |
6 | 3, 5 | bitri 263 |
. . . 4
⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(∪
𝐽 = ∪ 𝑦
→ ∃𝑧 ∈
(𝒫 𝐽 ∩
Fin)𝑧Ref𝑦))) |
7 | 6 | simprbi 479 |
. . 3
⊢ (𝐽 ∈ Comp →
∀𝑦 ∈ 𝒫
𝐽(∪ 𝐽 =
∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)𝑧Ref𝑦)) |
8 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → 𝑧 ∈ (𝒫 𝐽 ∩ Fin)) |
9 | | elin 3758 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ↔ (𝑧 ∈ 𝒫 𝐽 ∧ 𝑧 ∈ Fin)) |
10 | 8, 9 | sylib 207 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → (𝑧 ∈ 𝒫 𝐽 ∧ 𝑧 ∈ Fin)) |
11 | 10 | simpld 474 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → 𝑧 ∈ 𝒫 𝐽) |
12 | 1 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → 𝐽 ∈ Top) |
13 | 10 | simprd 478 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → 𝑧 ∈ Fin) |
14 | | simplr 788 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → ∪ 𝐽 = ∪
𝑦) |
15 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → 𝑧Ref𝑦) |
16 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑧 =
∪ 𝑧 |
17 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑦 =
∪ 𝑦 |
18 | 16, 17 | refbas 21123 |
. . . . . . . . . . . . 13
⊢ (𝑧Ref𝑦 → ∪ 𝑦 = ∪
𝑧) |
19 | 15, 18 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → ∪ 𝑦 = ∪
𝑧) |
20 | 14, 19 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → ∪ 𝐽 = ∪
𝑧) |
21 | 4, 16 | finlocfin 21133 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝑧 ∈ Fin ∧ ∪ 𝐽 =
∪ 𝑧) → 𝑧 ∈ (LocFin‘𝐽)) |
22 | 12, 13, 20, 21 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → 𝑧 ∈ (LocFin‘𝐽)) |
23 | 11, 22 | elind 3760 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → 𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽))) |
24 | 23, 15 | jca 553 |
. . . . . . . 8
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → (𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽)) ∧ 𝑧Ref𝑦)) |
25 | 24 | ex 449 |
. . . . . . 7
⊢ (((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) → ((𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦) → (𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽)) ∧ 𝑧Ref𝑦))) |
26 | 25 | reximdv2 2997 |
. . . . . 6
⊢ (((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) → (∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)𝑧Ref𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽))𝑧Ref𝑦)) |
27 | 26 | ex 449 |
. . . . 5
⊢ ((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) → (∪ 𝐽 =
∪ 𝑦 → (∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)𝑧Ref𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽))𝑧Ref𝑦))) |
28 | 27 | a2d 29 |
. . . 4
⊢ ((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) → ((∪ 𝐽 =
∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)𝑧Ref𝑦) → (∪ 𝐽 = ∪
𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽))𝑧Ref𝑦))) |
29 | 28 | ralimdva 2945 |
. . 3
⊢ (𝐽 ∈ Comp →
(∀𝑦 ∈ 𝒫
𝐽(∪ 𝐽 =
∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)𝑧Ref𝑦) → ∀𝑦 ∈ 𝒫 𝐽(∪ 𝐽 = ∪
𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽))𝑧Ref𝑦))) |
30 | 7, 29 | mpd 15 |
. 2
⊢ (𝐽 ∈ Comp →
∀𝑦 ∈ 𝒫
𝐽(∪ 𝐽 =
∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽))𝑧Ref𝑦)) |
31 | | ispcmp 29252 |
. . 3
⊢ (𝐽 ∈ Paracomp ↔ 𝐽 ∈
CovHasRef(LocFin‘𝐽)) |
32 | 4 | iscref 29239 |
. . 3
⊢ (𝐽 ∈
CovHasRef(LocFin‘𝐽)
↔ (𝐽 ∈ Top ∧
∀𝑦 ∈ 𝒫
𝐽(∪ 𝐽 =
∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽))𝑧Ref𝑦))) |
33 | 31, 32 | bitri 263 |
. 2
⊢ (𝐽 ∈ Paracomp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(∪
𝐽 = ∪ 𝑦
→ ∃𝑧 ∈
(𝒫 𝐽 ∩
(LocFin‘𝐽))𝑧Ref𝑦))) |
34 | 1, 30, 33 | sylanbrc 695 |
1
⊢ (𝐽 ∈ Comp → 𝐽 ∈
Paracomp) |