Step | Hyp | Ref
| Expression |
1 | | cmptop 22139 |
. 2
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
2 | | cmpcref 31364 |
. . . . . 6
⊢ Comp =
CovHasRefFin |
3 | 2 | eleq2i 2824 |
. . . . 5
⊢ (𝐽 ∈ Comp ↔ 𝐽 ∈
CovHasRefFin) |
4 | | eqid 2738 |
. . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 |
5 | 4 | iscref 31358 |
. . . . 5
⊢ (𝐽 ∈ CovHasRefFin ↔
(𝐽 ∈ Top ∧
∀𝑦 ∈ 𝒫
𝐽(∪ 𝐽 =
∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)𝑧Ref𝑦))) |
6 | 3, 5 | bitri 278 |
. . . 4
⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(∪
𝐽 = ∪ 𝑦
→ ∃𝑧 ∈
(𝒫 𝐽 ∩
Fin)𝑧Ref𝑦))) |
7 | 6 | simprbi 500 |
. . 3
⊢ (𝐽 ∈ Comp →
∀𝑦 ∈ 𝒫
𝐽(∪ 𝐽 =
∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)𝑧Ref𝑦)) |
8 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → 𝑧 ∈ (𝒫 𝐽 ∩ Fin)) |
9 | | elin 3857 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ↔ (𝑧 ∈ 𝒫 𝐽 ∧ 𝑧 ∈ Fin)) |
10 | 8, 9 | sylib 221 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → (𝑧 ∈ 𝒫 𝐽 ∧ 𝑧 ∈ Fin)) |
11 | 10 | simpld 498 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → 𝑧 ∈ 𝒫 𝐽) |
12 | 1 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → 𝐽 ∈ Top) |
13 | 10 | simprd 499 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → 𝑧 ∈ Fin) |
14 | | simplr 769 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → ∪ 𝐽 = ∪
𝑦) |
15 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → 𝑧Ref𝑦) |
16 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑧 =
∪ 𝑧 |
17 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑦 =
∪ 𝑦 |
18 | 16, 17 | refbas 22254 |
. . . . . . . . . . . . 13
⊢ (𝑧Ref𝑦 → ∪ 𝑦 = ∪
𝑧) |
19 | 15, 18 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → ∪ 𝑦 = ∪
𝑧) |
20 | 14, 19 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → ∪ 𝐽 = ∪
𝑧) |
21 | 4, 16 | finlocfin 22264 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝑧 ∈ Fin ∧ ∪ 𝐽 =
∪ 𝑧) → 𝑧 ∈ (LocFin‘𝐽)) |
22 | 12, 13, 20, 21 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → 𝑧 ∈ (LocFin‘𝐽)) |
23 | 11, 22 | elind 4082 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → 𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽))) |
24 | 23, 15 | jca 515 |
. . . . . . . 8
⊢ ((((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) ∧ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦)) → (𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽)) ∧ 𝑧Ref𝑦)) |
25 | 24 | ex 416 |
. . . . . . 7
⊢ (((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) → ((𝑧 ∈ (𝒫 𝐽 ∩ Fin) ∧ 𝑧Ref𝑦) → (𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽)) ∧ 𝑧Ref𝑦))) |
26 | 25 | reximdv2 3180 |
. . . . . 6
⊢ (((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) ∧ ∪ 𝐽 =
∪ 𝑦) → (∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)𝑧Ref𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽))𝑧Ref𝑦)) |
27 | 26 | ex 416 |
. . . . 5
⊢ ((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) → (∪ 𝐽 =
∪ 𝑦 → (∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)𝑧Ref𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽))𝑧Ref𝑦))) |
28 | 27 | a2d 29 |
. . . 4
⊢ ((𝐽 ∈ Comp ∧ 𝑦 ∈ 𝒫 𝐽) → ((∪ 𝐽 =
∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)𝑧Ref𝑦) → (∪ 𝐽 = ∪
𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽))𝑧Ref𝑦))) |
29 | 28 | ralimdva 3091 |
. . 3
⊢ (𝐽 ∈ Comp →
(∀𝑦 ∈ 𝒫
𝐽(∪ 𝐽 =
∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)𝑧Ref𝑦) → ∀𝑦 ∈ 𝒫 𝐽(∪ 𝐽 = ∪
𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽))𝑧Ref𝑦))) |
30 | 7, 29 | mpd 15 |
. 2
⊢ (𝐽 ∈ Comp →
∀𝑦 ∈ 𝒫
𝐽(∪ 𝐽 =
∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽))𝑧Ref𝑦)) |
31 | | ispcmp 31371 |
. . 3
⊢ (𝐽 ∈ Paracomp ↔ 𝐽 ∈
CovHasRef(LocFin‘𝐽)) |
32 | 4 | iscref 31358 |
. . 3
⊢ (𝐽 ∈
CovHasRef(LocFin‘𝐽)
↔ (𝐽 ∈ Top ∧
∀𝑦 ∈ 𝒫
𝐽(∪ 𝐽 =
∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ (LocFin‘𝐽))𝑧Ref𝑦))) |
33 | 31, 32 | bitri 278 |
. 2
⊢ (𝐽 ∈ Paracomp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(∪
𝐽 = ∪ 𝑦
→ ∃𝑧 ∈
(𝒫 𝐽 ∩
(LocFin‘𝐽))𝑧Ref𝑦))) |
34 | 1, 30, 33 | sylanbrc 586 |
1
⊢ (𝐽 ∈ Comp → 𝐽 ∈
Paracomp) |