Step | Hyp | Ref
| Expression |
1 | | eqid 2825 |
. . . . 5
⊢ ∪ (topGen‘(fi‘𝐵)) = ∪
(topGen‘(fi‘𝐵)) |
2 | 1 | iscmp 21562 |
. . . 4
⊢
((topGen‘(fi‘𝐵)) ∈ Comp ↔
((topGen‘(fi‘𝐵)) ∈ Top ∧ ∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(∪
(topGen‘(fi‘𝐵))
= ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪
(topGen‘(fi‘𝐵))
= ∪ 𝑦))) |
3 | 2 | simprbi 492 |
. . 3
⊢
((topGen‘(fi‘𝐵)) ∈ Comp → ∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(∪
(topGen‘(fi‘𝐵))
= ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪
(topGen‘(fi‘𝐵))
= ∪ 𝑦)) |
4 | | simpr 479 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝑋 = ∪ 𝐵) |
5 | | elex 3429 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ UFL → 𝑋 ∈ V) |
6 | 5 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝑋 ∈ V) |
7 | 4, 6 | eqeltrrd 2907 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → ∪ 𝐵
∈ V) |
8 | | uniexb 7233 |
. . . . . . . . . 10
⊢ (𝐵 ∈ V ↔ ∪ 𝐵
∈ V) |
9 | 7, 8 | sylibr 226 |
. . . . . . . . 9
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝐵 ∈ V) |
10 | | fiuni 8603 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → ∪ 𝐵 =
∪ (fi‘𝐵)) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → ∪ 𝐵 =
∪ (fi‘𝐵)) |
12 | | fibas 21152 |
. . . . . . . . 9
⊢
(fi‘𝐵) ∈
TopBases |
13 | | unitg 21142 |
. . . . . . . . 9
⊢
((fi‘𝐵) ∈
TopBases → ∪ (topGen‘(fi‘𝐵)) = ∪ (fi‘𝐵)) |
14 | 12, 13 | mp1i 13 |
. . . . . . . 8
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → ∪ (topGen‘(fi‘𝐵)) = ∪
(fi‘𝐵)) |
15 | 11, 4, 14 | 3eqtr4d 2871 |
. . . . . . 7
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝑋 = ∪
(topGen‘(fi‘𝐵))) |
16 | 15 | eqeq1d 2827 |
. . . . . 6
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (𝑋 = ∪
𝑥 ↔ ∪ (topGen‘(fi‘𝐵)) = ∪ 𝑥)) |
17 | 15 | eqeq1d 2827 |
. . . . . . 7
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (𝑋 = ∪
𝑦 ↔ ∪ (topGen‘(fi‘𝐵)) = ∪ 𝑦)) |
18 | 17 | rexbidv 3262 |
. . . . . 6
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦 ↔ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪ (topGen‘(fi‘𝐵)) = ∪ 𝑦)) |
19 | 16, 18 | imbi12d 336 |
. . . . 5
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → ((𝑋 = ∪
𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) ↔ (∪ (topGen‘(fi‘𝐵)) = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪ (topGen‘(fi‘𝐵)) = ∪ 𝑦))) |
20 | 19 | ralbidv 3195 |
. . . 4
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) ↔ ∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(∪
(topGen‘(fi‘𝐵))
= ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪
(topGen‘(fi‘𝐵))
= ∪ 𝑦))) |
21 | | ssfii 8594 |
. . . . . . . 8
⊢ (𝐵 ∈ V → 𝐵 ⊆ (fi‘𝐵)) |
22 | 9, 21 | syl 17 |
. . . . . . 7
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝐵 ⊆ (fi‘𝐵)) |
23 | | bastg 21141 |
. . . . . . . 8
⊢
((fi‘𝐵) ∈
TopBases → (fi‘𝐵) ⊆ (topGen‘(fi‘𝐵))) |
24 | 12, 23 | ax-mp 5 |
. . . . . . 7
⊢
(fi‘𝐵) ⊆
(topGen‘(fi‘𝐵)) |
25 | 22, 24 | syl6ss 3839 |
. . . . . 6
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝐵 ⊆ (topGen‘(fi‘𝐵))) |
26 | | sspwb 5138 |
. . . . . 6
⊢ (𝐵 ⊆
(topGen‘(fi‘𝐵))
↔ 𝒫 𝐵 ⊆
𝒫 (topGen‘(fi‘𝐵))) |
27 | 25, 26 | sylib 210 |
. . . . 5
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝒫 𝐵 ⊆ 𝒫
(topGen‘(fi‘𝐵))) |
28 | | ssralv 3891 |
. . . . 5
⊢
(𝒫 𝐵 ⊆
𝒫 (topGen‘(fi‘𝐵)) → (∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) → ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) |
29 | 27, 28 | syl 17 |
. . . 4
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) → ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) |
30 | 20, 29 | sylbird 252 |
. . 3
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(∪
(topGen‘(fi‘𝐵))
= ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪
(topGen‘(fi‘𝐵))
= ∪ 𝑦) → ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) |
31 | 3, 30 | syl5 34 |
. 2
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) →
((topGen‘(fi‘𝐵)) ∈ Comp → ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) |
32 | | simpll 783 |
. . . 4
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) → 𝑋 ∈ UFL) |
33 | | simplr 785 |
. . . 4
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) → 𝑋 = ∪ 𝐵) |
34 | | eqidd 2826 |
. . . 4
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) →
(topGen‘(fi‘𝐵))
= (topGen‘(fi‘𝐵))) |
35 | | selpw 4385 |
. . . . . . 7
⊢ (𝑧 ∈ 𝒫 𝐵 ↔ 𝑧 ⊆ 𝐵) |
36 | | unieq 4666 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ∪ 𝑥 = ∪
𝑧) |
37 | 36 | eqeq2d 2835 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑋 = ∪ 𝑥 ↔ 𝑋 = ∪ 𝑧)) |
38 | | pweq 4381 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → 𝒫 𝑥 = 𝒫 𝑧) |
39 | 38 | ineq1d 4040 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝒫 𝑥 ∩ Fin) = (𝒫 𝑧 ∩ Fin)) |
40 | 39 | rexeqdv 3357 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦 ↔ ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦)) |
41 | 37, 40 | imbi12d 336 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → ((𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) ↔ (𝑋 = ∪ 𝑧 → ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦))) |
42 | 41 | rspccv 3523 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝒫 𝐵(𝑋 = ∪
𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) → (𝑧 ∈ 𝒫 𝐵 → (𝑋 = ∪ 𝑧 → ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦))) |
43 | 42 | adantl 475 |
. . . . . . 7
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) → (𝑧 ∈ 𝒫 𝐵 → (𝑋 = ∪ 𝑧 → ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦))) |
44 | 35, 43 | syl5bir 235 |
. . . . . 6
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) → (𝑧 ⊆ 𝐵 → (𝑋 = ∪ 𝑧 → ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦))) |
45 | 44 | imp32 411 |
. . . . 5
⊢ ((((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) ∧ (𝑧 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑧)) → ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦) |
46 | | unieq 4666 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → ∪ 𝑦 = ∪
𝑤) |
47 | 46 | eqeq2d 2835 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑤)) |
48 | 47 | cbvrexv 3384 |
. . . . 5
⊢
(∃𝑦 ∈
(𝒫 𝑧 ∩
Fin)𝑋 = ∪ 𝑦
↔ ∃𝑤 ∈
(𝒫 𝑧 ∩
Fin)𝑋 = ∪ 𝑤) |
49 | 45, 48 | sylib 210 |
. . . 4
⊢ ((((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) ∧ (𝑧 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑧)) → ∃𝑤 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑤) |
50 | 32, 33, 34, 49 | alexsub 22219 |
. . 3
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) →
(topGen‘(fi‘𝐵))
∈ Comp) |
51 | 50 | ex 403 |
. 2
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) →
(topGen‘(fi‘𝐵))
∈ Comp)) |
52 | 31, 51 | impbid 204 |
1
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) →
((topGen‘(fi‘𝐵)) ∈ Comp ↔ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) |