| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . . 5
⊢ ∪ (topGen‘(fi‘𝐵)) = ∪
(topGen‘(fi‘𝐵)) | 
| 2 | 1 | iscmp 23397 | . . . 4
⊢
((topGen‘(fi‘𝐵)) ∈ Comp ↔
((topGen‘(fi‘𝐵)) ∈ Top ∧ ∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(∪
(topGen‘(fi‘𝐵))
= ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪
(topGen‘(fi‘𝐵))
= ∪ 𝑦))) | 
| 3 | 2 | simprbi 496 | . . 3
⊢
((topGen‘(fi‘𝐵)) ∈ Comp → ∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(∪
(topGen‘(fi‘𝐵))
= ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪
(topGen‘(fi‘𝐵))
= ∪ 𝑦)) | 
| 4 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝑋 = ∪ 𝐵) | 
| 5 |  | elex 3500 | . . . . . . . . . . . 12
⊢ (𝑋 ∈ UFL → 𝑋 ∈ V) | 
| 6 | 5 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝑋 ∈ V) | 
| 7 | 4, 6 | eqeltrrd 2841 | . . . . . . . . . 10
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → ∪ 𝐵
∈ V) | 
| 8 |  | uniexb 7785 | . . . . . . . . . 10
⊢ (𝐵 ∈ V ↔ ∪ 𝐵
∈ V) | 
| 9 | 7, 8 | sylibr 234 | . . . . . . . . 9
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝐵 ∈ V) | 
| 10 |  | fiuni 9469 | . . . . . . . . 9
⊢ (𝐵 ∈ V → ∪ 𝐵 =
∪ (fi‘𝐵)) | 
| 11 | 9, 10 | syl 17 | . . . . . . . 8
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → ∪ 𝐵 =
∪ (fi‘𝐵)) | 
| 12 |  | fibas 22985 | . . . . . . . . 9
⊢
(fi‘𝐵) ∈
TopBases | 
| 13 |  | unitg 22975 | . . . . . . . . 9
⊢
((fi‘𝐵) ∈
TopBases → ∪ (topGen‘(fi‘𝐵)) = ∪ (fi‘𝐵)) | 
| 14 | 12, 13 | mp1i 13 | . . . . . . . 8
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → ∪ (topGen‘(fi‘𝐵)) = ∪
(fi‘𝐵)) | 
| 15 | 11, 4, 14 | 3eqtr4d 2786 | . . . . . . 7
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝑋 = ∪
(topGen‘(fi‘𝐵))) | 
| 16 | 15 | eqeq1d 2738 | . . . . . 6
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (𝑋 = ∪
𝑥 ↔ ∪ (topGen‘(fi‘𝐵)) = ∪ 𝑥)) | 
| 17 | 15 | eqeq1d 2738 | . . . . . . 7
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (𝑋 = ∪
𝑦 ↔ ∪ (topGen‘(fi‘𝐵)) = ∪ 𝑦)) | 
| 18 | 17 | rexbidv 3178 | . . . . . 6
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦 ↔ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪ (topGen‘(fi‘𝐵)) = ∪ 𝑦)) | 
| 19 | 16, 18 | imbi12d 344 | . . . . 5
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → ((𝑋 = ∪
𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) ↔ (∪ (topGen‘(fi‘𝐵)) = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪ (topGen‘(fi‘𝐵)) = ∪ 𝑦))) | 
| 20 | 19 | ralbidv 3177 | . . . 4
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) ↔ ∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(∪
(topGen‘(fi‘𝐵))
= ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪
(topGen‘(fi‘𝐵))
= ∪ 𝑦))) | 
| 21 |  | ssfii 9460 | . . . . . . . 8
⊢ (𝐵 ∈ V → 𝐵 ⊆ (fi‘𝐵)) | 
| 22 | 9, 21 | syl 17 | . . . . . . 7
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝐵 ⊆ (fi‘𝐵)) | 
| 23 |  | bastg 22974 | . . . . . . . 8
⊢
((fi‘𝐵) ∈
TopBases → (fi‘𝐵) ⊆ (topGen‘(fi‘𝐵))) | 
| 24 | 12, 23 | ax-mp 5 | . . . . . . 7
⊢
(fi‘𝐵) ⊆
(topGen‘(fi‘𝐵)) | 
| 25 | 22, 24 | sstrdi 3995 | . . . . . 6
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝐵 ⊆ (topGen‘(fi‘𝐵))) | 
| 26 | 25 | sspwd 4612 | . . . . 5
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝒫 𝐵 ⊆ 𝒫
(topGen‘(fi‘𝐵))) | 
| 27 |  | ssralv 4051 | . . . . 5
⊢
(𝒫 𝐵 ⊆
𝒫 (topGen‘(fi‘𝐵)) → (∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) → ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) | 
| 28 | 26, 27 | syl 17 | . . . 4
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) → ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) | 
| 29 | 20, 28 | sylbird 260 | . . 3
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(∪
(topGen‘(fi‘𝐵))
= ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪
(topGen‘(fi‘𝐵))
= ∪ 𝑦) → ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) | 
| 30 | 3, 29 | syl5 34 | . 2
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) →
((topGen‘(fi‘𝐵)) ∈ Comp → ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) | 
| 31 |  | simpll 766 | . . . 4
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) → 𝑋 ∈ UFL) | 
| 32 |  | simplr 768 | . . . 4
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) → 𝑋 = ∪ 𝐵) | 
| 33 |  | eqidd 2737 | . . . 4
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) →
(topGen‘(fi‘𝐵))
= (topGen‘(fi‘𝐵))) | 
| 34 |  | velpw 4604 | . . . . . . 7
⊢ (𝑧 ∈ 𝒫 𝐵 ↔ 𝑧 ⊆ 𝐵) | 
| 35 |  | unieq 4917 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ∪ 𝑥 = ∪
𝑧) | 
| 36 | 35 | eqeq2d 2747 | . . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑋 = ∪ 𝑥 ↔ 𝑋 = ∪ 𝑧)) | 
| 37 |  | pweq 4613 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → 𝒫 𝑥 = 𝒫 𝑧) | 
| 38 | 37 | ineq1d 4218 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝒫 𝑥 ∩ Fin) = (𝒫 𝑧 ∩ Fin)) | 
| 39 | 38 | rexeqdv 3326 | . . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦 ↔ ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦)) | 
| 40 | 36, 39 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑥 = 𝑧 → ((𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) ↔ (𝑋 = ∪ 𝑧 → ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦))) | 
| 41 | 40 | rspccv 3618 | . . . . . . . 8
⊢
(∀𝑥 ∈
𝒫 𝐵(𝑋 = ∪
𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) → (𝑧 ∈ 𝒫 𝐵 → (𝑋 = ∪ 𝑧 → ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦))) | 
| 42 | 41 | adantl 481 | . . . . . . 7
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) → (𝑧 ∈ 𝒫 𝐵 → (𝑋 = ∪ 𝑧 → ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦))) | 
| 43 | 34, 42 | biimtrrid 243 | . . . . . 6
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) → (𝑧 ⊆ 𝐵 → (𝑋 = ∪ 𝑧 → ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦))) | 
| 44 | 43 | imp32 418 | . . . . 5
⊢ ((((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) ∧ (𝑧 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑧)) → ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦) | 
| 45 |  | unieq 4917 | . . . . . . 7
⊢ (𝑦 = 𝑤 → ∪ 𝑦 = ∪
𝑤) | 
| 46 | 45 | eqeq2d 2747 | . . . . . 6
⊢ (𝑦 = 𝑤 → (𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑤)) | 
| 47 | 46 | cbvrexvw 3237 | . . . . 5
⊢
(∃𝑦 ∈
(𝒫 𝑧 ∩
Fin)𝑋 = ∪ 𝑦
↔ ∃𝑤 ∈
(𝒫 𝑧 ∩
Fin)𝑋 = ∪ 𝑤) | 
| 48 | 44, 47 | sylib 218 | . . . 4
⊢ ((((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) ∧ (𝑧 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑧)) → ∃𝑤 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑤) | 
| 49 | 31, 32, 33, 48 | alexsub 24054 | . . 3
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) →
(topGen‘(fi‘𝐵))
∈ Comp) | 
| 50 | 49 | ex 412 | . 2
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) →
(topGen‘(fi‘𝐵))
∈ Comp)) | 
| 51 | 30, 50 | impbid 212 | 1
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) →
((topGen‘(fi‘𝐵)) ∈ Comp ↔ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) |