| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | distop 23003 | . . 3
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Top) | 
| 2 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑢 = {𝑥}) → 𝑢 = {𝑥}) | 
| 3 |  | snelpwi 5447 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑋 → {𝑥} ∈ 𝒫 𝑋) | 
| 4 | 3 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑢 = {𝑥}) → {𝑥} ∈ 𝒫 𝑋) | 
| 5 | 2, 4 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑢 = {𝑥}) → 𝑢 ∈ 𝒫 𝑋) | 
| 6 | 5 | rexlimiva 3146 | . . . . . . . . . 10
⊢
(∃𝑥 ∈
𝑋 𝑢 = {𝑥} → 𝑢 ∈ 𝒫 𝑋) | 
| 7 | 6 | abssi 4069 | . . . . . . . . 9
⊢ {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} ⊆ 𝒫 𝑋 | 
| 8 |  | simpl 482 | . . . . . . . . . . . . . 14
⊢ ((𝑢 = 𝑣 ∧ 𝑥 = 𝑧) → 𝑢 = 𝑣) | 
| 9 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝑢 = 𝑣 ∧ 𝑥 = 𝑧) → 𝑥 = 𝑧) | 
| 10 | 9 | sneqd 4637 | . . . . . . . . . . . . . 14
⊢ ((𝑢 = 𝑣 ∧ 𝑥 = 𝑧) → {𝑥} = {𝑧}) | 
| 11 | 8, 10 | eqeq12d 2752 | . . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑣 ∧ 𝑥 = 𝑧) → (𝑢 = {𝑥} ↔ 𝑣 = {𝑧})) | 
| 12 | 11 | cbvrexdva 3239 | . . . . . . . . . . . 12
⊢ (𝑢 = 𝑣 → (∃𝑥 ∈ 𝑋 𝑢 = {𝑥} ↔ ∃𝑧 ∈ 𝑋 𝑣 = {𝑧})) | 
| 13 | 12 | cbvabv 2811 | . . . . . . . . . . 11
⊢ {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} = {𝑣 ∣ ∃𝑧 ∈ 𝑋 𝑣 = {𝑧}} | 
| 14 | 13 | dissnlocfin 23538 | . . . . . . . . . 10
⊢ (𝑋 ∈ 𝑉 → {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} ∈ (LocFin‘𝒫 𝑋)) | 
| 15 |  | elpwg 4602 | . . . . . . . . . 10
⊢ ({𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} ∈ (LocFin‘𝒫 𝑋) → ({𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} ∈ 𝒫 𝒫 𝑋 ↔ {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} ⊆ 𝒫 𝑋)) | 
| 16 | 14, 15 | syl 17 | . . . . . . . . 9
⊢ (𝑋 ∈ 𝑉 → ({𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} ∈ 𝒫 𝒫 𝑋 ↔ {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} ⊆ 𝒫 𝑋)) | 
| 17 | 7, 16 | mpbiri 258 | . . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} ∈ 𝒫 𝒫 𝑋) | 
| 18 | 17 | ad2antrr 726 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋) ∧ 𝑋 = ∪ 𝑦) → {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} ∈ 𝒫 𝒫 𝑋) | 
| 19 | 14 | ad2antrr 726 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋) ∧ 𝑋 = ∪ 𝑦) → {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} ∈ (LocFin‘𝒫 𝑋)) | 
| 20 | 18, 19 | elind 4199 | . . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋) ∧ 𝑋 = ∪ 𝑦) → {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} ∈ (𝒫 𝒫 𝑋 ∩ (LocFin‘𝒫
𝑋))) | 
| 21 |  | simpll 766 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋) ∧ 𝑋 = ∪ 𝑦) → 𝑋 ∈ 𝑉) | 
| 22 |  | simpr 484 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋) ∧ 𝑋 = ∪ 𝑦) → 𝑋 = ∪ 𝑦) | 
| 23 | 22 | eqcomd 2742 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋) ∧ 𝑋 = ∪ 𝑦) → ∪ 𝑦 =
𝑋) | 
| 24 | 13 | dissnref 23537 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ ∪ 𝑦 = 𝑋) → {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}}Ref𝑦) | 
| 25 | 21, 23, 24 | syl2anc 584 | . . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋) ∧ 𝑋 = ∪ 𝑦) → {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}}Ref𝑦) | 
| 26 |  | breq1 5145 | . . . . . . 7
⊢ (𝑧 = {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} → (𝑧Ref𝑦 ↔ {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}}Ref𝑦)) | 
| 27 | 26 | rspcev 3621 | . . . . . 6
⊢ (({𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} ∈ (𝒫 𝒫 𝑋 ∩ (LocFin‘𝒫
𝑋)) ∧ {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}}Ref𝑦) → ∃𝑧 ∈ (𝒫 𝒫 𝑋 ∩ (LocFin‘𝒫
𝑋))𝑧Ref𝑦) | 
| 28 | 20, 25, 27 | syl2anc 584 | . . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋) ∧ 𝑋 = ∪ 𝑦) → ∃𝑧 ∈ (𝒫 𝒫
𝑋 ∩
(LocFin‘𝒫 𝑋))𝑧Ref𝑦) | 
| 29 | 28 | ex 412 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝒫
𝑋 ∩
(LocFin‘𝒫 𝑋))𝑧Ref𝑦)) | 
| 30 | 29 | ralrimiva 3145 | . . 3
⊢ (𝑋 ∈ 𝑉 → ∀𝑦 ∈ 𝒫 𝒫 𝑋(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝒫
𝑋 ∩
(LocFin‘𝒫 𝑋))𝑧Ref𝑦)) | 
| 31 |  | unipw 5454 | . . . . 5
⊢ ∪ 𝒫 𝑋 = 𝑋 | 
| 32 | 31 | eqcomi 2745 | . . . 4
⊢ 𝑋 = ∪
𝒫 𝑋 | 
| 33 | 32 | iscref 33844 | . . 3
⊢
(𝒫 𝑋 ∈
CovHasRef(LocFin‘𝒫 𝑋) ↔ (𝒫 𝑋 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝒫 𝑋(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝒫
𝑋 ∩
(LocFin‘𝒫 𝑋))𝑧Ref𝑦))) | 
| 34 | 1, 30, 33 | sylanbrc 583 | . 2
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ CovHasRef(LocFin‘𝒫
𝑋)) | 
| 35 |  | ispcmp 33857 | . 2
⊢
(𝒫 𝑋 ∈
Paracomp ↔ 𝒫 𝑋
∈ CovHasRef(LocFin‘𝒫 𝑋)) | 
| 36 | 34, 35 | sylibr 234 | 1
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Paracomp) |