Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢ ∪ (topGen‘(fi‘𝐵)) = ∪
(topGen‘(fi‘𝐵)) |
2 | 1 | iscmp 21001 |
. . . 4
⊢
((topGen‘(fi‘𝐵)) ∈ Comp ↔
((topGen‘(fi‘𝐵)) ∈ Top ∧ ∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(∪
(topGen‘(fi‘𝐵))
= ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪
(topGen‘(fi‘𝐵))
= ∪ 𝑦))) |
3 | 2 | simprbi 479 |
. . 3
⊢
((topGen‘(fi‘𝐵)) ∈ Comp → ∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(∪
(topGen‘(fi‘𝐵))
= ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪
(topGen‘(fi‘𝐵))
= ∪ 𝑦)) |
4 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝑋 = ∪ 𝐵) |
5 | | elex 3185 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ UFL → 𝑋 ∈ V) |
6 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝑋 ∈ V) |
7 | 4, 6 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → ∪ 𝐵
∈ V) |
8 | | uniexb 6866 |
. . . . . . . . . 10
⊢ (𝐵 ∈ V ↔ ∪ 𝐵
∈ V) |
9 | 7, 8 | sylibr 223 |
. . . . . . . . 9
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝐵 ∈ V) |
10 | | fiuni 8217 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → ∪ 𝐵 =
∪ (fi‘𝐵)) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → ∪ 𝐵 =
∪ (fi‘𝐵)) |
12 | | fibas 20592 |
. . . . . . . . 9
⊢
(fi‘𝐵) ∈
TopBases |
13 | | unitg 20582 |
. . . . . . . . 9
⊢
((fi‘𝐵) ∈
TopBases → ∪ (topGen‘(fi‘𝐵)) = ∪ (fi‘𝐵)) |
14 | 12, 13 | mp1i 13 |
. . . . . . . 8
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → ∪ (topGen‘(fi‘𝐵)) = ∪
(fi‘𝐵)) |
15 | 11, 4, 14 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝑋 = ∪
(topGen‘(fi‘𝐵))) |
16 | 15 | eqeq1d 2612 |
. . . . . 6
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (𝑋 = ∪
𝑥 ↔ ∪ (topGen‘(fi‘𝐵)) = ∪ 𝑥)) |
17 | 15 | eqeq1d 2612 |
. . . . . . 7
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (𝑋 = ∪
𝑦 ↔ ∪ (topGen‘(fi‘𝐵)) = ∪ 𝑦)) |
18 | 17 | rexbidv 3034 |
. . . . . 6
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦 ↔ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪ (topGen‘(fi‘𝐵)) = ∪ 𝑦)) |
19 | 16, 18 | imbi12d 333 |
. . . . 5
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → ((𝑋 = ∪
𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) ↔ (∪ (topGen‘(fi‘𝐵)) = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪ (topGen‘(fi‘𝐵)) = ∪ 𝑦))) |
20 | 19 | ralbidv 2969 |
. . . 4
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) ↔ ∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(∪
(topGen‘(fi‘𝐵))
= ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪
(topGen‘(fi‘𝐵))
= ∪ 𝑦))) |
21 | | ssfii 8208 |
. . . . . . . 8
⊢ (𝐵 ∈ V → 𝐵 ⊆ (fi‘𝐵)) |
22 | 9, 21 | syl 17 |
. . . . . . 7
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝐵 ⊆ (fi‘𝐵)) |
23 | | bastg 20581 |
. . . . . . . 8
⊢
((fi‘𝐵) ∈
TopBases → (fi‘𝐵) ⊆ (topGen‘(fi‘𝐵))) |
24 | 12, 23 | ax-mp 5 |
. . . . . . 7
⊢
(fi‘𝐵) ⊆
(topGen‘(fi‘𝐵)) |
25 | 22, 24 | syl6ss 3580 |
. . . . . 6
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝐵 ⊆ (topGen‘(fi‘𝐵))) |
26 | | sspwb 4844 |
. . . . . 6
⊢ (𝐵 ⊆
(topGen‘(fi‘𝐵))
↔ 𝒫 𝐵 ⊆
𝒫 (topGen‘(fi‘𝐵))) |
27 | 25, 26 | sylib 207 |
. . . . 5
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → 𝒫 𝐵 ⊆ 𝒫
(topGen‘(fi‘𝐵))) |
28 | | ssralv 3629 |
. . . . 5
⊢
(𝒫 𝐵 ⊆
𝒫 (topGen‘(fi‘𝐵)) → (∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) → ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) |
29 | 27, 28 | syl 17 |
. . . 4
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) → ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) |
30 | 20, 29 | sylbird 249 |
. . 3
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (∀𝑥 ∈ 𝒫
(topGen‘(fi‘𝐵))(∪
(topGen‘(fi‘𝐵))
= ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)∪
(topGen‘(fi‘𝐵))
= ∪ 𝑦) → ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) |
31 | 3, 30 | syl5 33 |
. 2
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) →
((topGen‘(fi‘𝐵)) ∈ Comp → ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) |
32 | | simpll 786 |
. . . 4
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) → 𝑋 ∈ UFL) |
33 | | simplr 788 |
. . . 4
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) → 𝑋 = ∪ 𝐵) |
34 | | eqidd 2611 |
. . . 4
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) →
(topGen‘(fi‘𝐵))
= (topGen‘(fi‘𝐵))) |
35 | | selpw 4115 |
. . . . . . 7
⊢ (𝑧 ∈ 𝒫 𝐵 ↔ 𝑧 ⊆ 𝐵) |
36 | | unieq 4380 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ∪ 𝑥 = ∪
𝑧) |
37 | 36 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑋 = ∪ 𝑥 ↔ 𝑋 = ∪ 𝑧)) |
38 | | pweq 4111 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → 𝒫 𝑥 = 𝒫 𝑧) |
39 | 38 | ineq1d 3775 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝒫 𝑥 ∩ Fin) = (𝒫 𝑧 ∩ Fin)) |
40 | 39 | rexeqdv 3122 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦 ↔ ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦)) |
41 | 37, 40 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → ((𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) ↔ (𝑋 = ∪ 𝑧 → ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦))) |
42 | 41 | rspccv 3279 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝒫 𝐵(𝑋 = ∪
𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) → (𝑧 ∈ 𝒫 𝐵 → (𝑋 = ∪ 𝑧 → ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦))) |
43 | 42 | adantl 481 |
. . . . . . 7
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) → (𝑧 ∈ 𝒫 𝐵 → (𝑋 = ∪ 𝑧 → ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦))) |
44 | 35, 43 | syl5bir 232 |
. . . . . 6
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) → (𝑧 ⊆ 𝐵 → (𝑋 = ∪ 𝑧 → ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦))) |
45 | 44 | imp32 448 |
. . . . 5
⊢ ((((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) ∧ (𝑧 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑧)) → ∃𝑦 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑦) |
46 | | unieq 4380 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → ∪ 𝑦 = ∪
𝑤) |
47 | 46 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑤)) |
48 | 47 | cbvrexv 3148 |
. . . . 5
⊢
(∃𝑦 ∈
(𝒫 𝑧 ∩
Fin)𝑋 = ∪ 𝑦
↔ ∃𝑤 ∈
(𝒫 𝑧 ∩
Fin)𝑋 = ∪ 𝑤) |
49 | 45, 48 | sylib 207 |
. . . 4
⊢ ((((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) ∧ (𝑧 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑧)) → ∃𝑤 ∈ (𝒫 𝑧 ∩ Fin)𝑋 = ∪ 𝑤) |
50 | 32, 33, 34, 49 | alexsub 21659 |
. . 3
⊢ (((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) ∧ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)) →
(topGen‘(fi‘𝐵))
∈ Comp) |
51 | 50 | ex 449 |
. 2
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) → (∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) →
(topGen‘(fi‘𝐵))
∈ Comp)) |
52 | 31, 51 | impbid 201 |
1
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪
𝐵) →
((topGen‘(fi‘𝐵)) ∈ Comp ↔ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) |