Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . . 5
⊢ ∪ (topGen‘𝐵) = ∪
(topGen‘𝐵) |
2 | 1 | iscmp 22539 |
. . . 4
⊢
((topGen‘𝐵)
∈ Comp ↔ ((topGen‘𝐵) ∈ Top ∧ ∀𝑦 ∈ 𝒫
(topGen‘𝐵)(∪ (topGen‘𝐵) = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑧))) |
3 | 2 | simprbi 497 |
. . 3
⊢
((topGen‘𝐵)
∈ Comp → ∀𝑦 ∈ 𝒫 (topGen‘𝐵)(∪
(topGen‘𝐵) = ∪ 𝑦
→ ∃𝑧 ∈
(𝒫 𝑦 ∩
Fin)∪ (topGen‘𝐵) = ∪ 𝑧)) |
4 | | unitg 22117 |
. . . . . . . 8
⊢ (𝐵 ∈ TopBases → ∪ (topGen‘𝐵) = ∪ 𝐵) |
5 | | eqtr3 2764 |
. . . . . . . 8
⊢ ((∪ (topGen‘𝐵) = ∪ 𝐵 ∧ 𝑋 = ∪ 𝐵) → ∪ (topGen‘𝐵) = 𝑋) |
6 | 4, 5 | sylan 580 |
. . . . . . 7
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → ∪ (topGen‘𝐵) = 𝑋) |
7 | 6 | eqeq1d 2740 |
. . . . . 6
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → (∪ (topGen‘𝐵) = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑦)) |
8 | 6 | eqeq1d 2740 |
. . . . . . 7
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → (∪ (topGen‘𝐵) = ∪ 𝑧 ↔ 𝑋 = ∪ 𝑧)) |
9 | 8 | rexbidv 3226 |
. . . . . 6
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
10 | 7, 9 | imbi12d 345 |
. . . . 5
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → ((∪ (topGen‘𝐵) = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑧) ↔ (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |
11 | 10 | ralbidv 3112 |
. . . 4
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → (∀𝑦 ∈ 𝒫
(topGen‘𝐵)(∪ (topGen‘𝐵) = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑧) ↔ ∀𝑦 ∈ 𝒫
(topGen‘𝐵)(𝑋 = ∪
𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |
12 | | bastg 22116 |
. . . . . . 7
⊢ (𝐵 ∈ TopBases → 𝐵 ⊆ (topGen‘𝐵)) |
13 | 12 | adantr 481 |
. . . . . 6
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → 𝐵 ⊆ (topGen‘𝐵)) |
14 | 13 | sspwd 4548 |
. . . . 5
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → 𝒫 𝐵 ⊆ 𝒫
(topGen‘𝐵)) |
15 | | ssralv 3987 |
. . . . 5
⊢
(𝒫 𝐵 ⊆
𝒫 (topGen‘𝐵)
→ (∀𝑦 ∈
𝒫 (topGen‘𝐵)(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |
16 | 14, 15 | syl 17 |
. . . 4
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → (∀𝑦 ∈ 𝒫
(topGen‘𝐵)(𝑋 = ∪
𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |
17 | 11, 16 | sylbid 239 |
. . 3
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → (∀𝑦 ∈ 𝒫
(topGen‘𝐵)(∪ (topGen‘𝐵) = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑧) → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |
18 | 3, 17 | syl5 34 |
. 2
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) →
((topGen‘𝐵) ∈
Comp → ∀𝑦
∈ 𝒫 𝐵(𝑋 = ∪
𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |
19 | | elpwi 4542 |
. . . . 5
⊢ (𝑢 ∈ 𝒫
(topGen‘𝐵) →
𝑢 ⊆
(topGen‘𝐵)) |
20 | | simprr 770 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → 𝑋 = ∪ 𝑢) |
21 | | simprl 768 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → 𝑢 ⊆ (topGen‘𝐵)) |
22 | 21 | sselda 3921 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ (topGen‘𝐵)) |
23 | 22 | adantrr 714 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑦 ∈ 𝑡)) → 𝑡 ∈ (topGen‘𝐵)) |
24 | | simprr 770 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑦 ∈ 𝑡)) → 𝑦 ∈ 𝑡) |
25 | | tg2 22115 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ (topGen‘𝐵) ∧ 𝑦 ∈ 𝑡) → ∃𝑤 ∈ 𝐵 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡)) |
26 | 23, 24, 25 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑦 ∈ 𝑡)) → ∃𝑤 ∈ 𝐵 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡)) |
27 | 26 | expr 457 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ 𝑡 ∈ 𝑢) → (𝑦 ∈ 𝑡 → ∃𝑤 ∈ 𝐵 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡))) |
28 | 27 | reximdva 3203 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → (∃𝑡 ∈ 𝑢 𝑦 ∈ 𝑡 → ∃𝑡 ∈ 𝑢 ∃𝑤 ∈ 𝐵 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡))) |
29 | | eluni2 4843 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ∪ 𝑢
↔ ∃𝑡 ∈
𝑢 𝑦 ∈ 𝑡) |
30 | | elunirab 4855 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ∪ {𝑤
∈ 𝐵 ∣
∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ↔ ∃𝑤 ∈ 𝐵 (𝑦 ∈ 𝑤 ∧ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡)) |
31 | | r19.42v 3279 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑡 ∈
𝑢 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡) ↔ (𝑦 ∈ 𝑤 ∧ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡)) |
32 | 31 | rexbii 3181 |
. . . . . . . . . . . . . 14
⊢
(∃𝑤 ∈
𝐵 ∃𝑡 ∈ 𝑢 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡) ↔ ∃𝑤 ∈ 𝐵 (𝑦 ∈ 𝑤 ∧ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡)) |
33 | | rexcom 3234 |
. . . . . . . . . . . . . 14
⊢
(∃𝑤 ∈
𝐵 ∃𝑡 ∈ 𝑢 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡) ↔ ∃𝑡 ∈ 𝑢 ∃𝑤 ∈ 𝐵 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡)) |
34 | 30, 32, 33 | 3bitr2i 299 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ∪ {𝑤
∈ 𝐵 ∣
∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ↔ ∃𝑡 ∈ 𝑢 ∃𝑤 ∈ 𝐵 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡)) |
35 | 28, 29, 34 | 3imtr4g 296 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → (𝑦 ∈ ∪ 𝑢 → 𝑦 ∈ ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡})) |
36 | 35 | ssrdv 3927 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → ∪ 𝑢
⊆ ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡}) |
37 | 20, 36 | eqsstrd 3959 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → 𝑋 ⊆ ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡}) |
38 | | ssrab2 4013 |
. . . . . . . . . . . 12
⊢ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ⊆ 𝐵 |
39 | 38 | unissi 4848 |
. . . . . . . . . . 11
⊢ ∪ {𝑤
∈ 𝐵 ∣
∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ⊆ ∪ 𝐵 |
40 | | simplr 766 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → 𝑋 = ∪ 𝐵) |
41 | 39, 40 | sseqtrrid 3974 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → ∪ {𝑤
∈ 𝐵 ∣
∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ⊆ 𝑋) |
42 | 37, 41 | eqssd 3938 |
. . . . . . . . 9
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → 𝑋 = ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡}) |
43 | | elpw2g 5268 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ TopBases → ({𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∈ 𝒫 𝐵 ↔ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ⊆ 𝐵)) |
44 | 43 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → ({𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∈ 𝒫 𝐵 ↔ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ⊆ 𝐵)) |
45 | 38, 44 | mpbiri 257 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∈ 𝒫 𝐵) |
46 | | unieq 4850 |
. . . . . . . . . . . . 13
⊢ (𝑦 = {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → ∪ 𝑦 = ∪
{𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡}) |
47 | 46 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ (𝑦 = {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → (𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡})) |
48 | | pweq 4549 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → 𝒫 𝑦 = 𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡}) |
49 | 48 | ineq1d 4145 |
. . . . . . . . . . . . 13
⊢ (𝑦 = {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → (𝒫 𝑦 ∩ Fin) = (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin)) |
50 | 49 | rexeqdv 3349 |
. . . . . . . . . . . 12
⊢ (𝑦 = {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin)𝑋 = ∪ 𝑧)) |
51 | 47, 50 | imbi12d 345 |
. . . . . . . . . . 11
⊢ (𝑦 = {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → ((𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) ↔ (𝑋 = ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → ∃𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin)𝑋 = ∪ 𝑧))) |
52 | 51 | rspcv 3557 |
. . . . . . . . . 10
⊢ ({𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∈ 𝒫 𝐵 → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → (𝑋 = ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → ∃𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin)𝑋 = ∪ 𝑧))) |
53 | 45, 52 | syl 17 |
. . . . . . . . 9
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → (𝑋 = ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → ∃𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin)𝑋 = ∪ 𝑧))) |
54 | 42, 53 | mpid 44 |
. . . . . . . 8
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → ∃𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin)𝑋 = ∪ 𝑧)) |
55 | | elfpw 9121 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ↔ (𝑧 ⊆ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∧ 𝑧 ∈ Fin)) |
56 | 55 | simprbi 497 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) → 𝑧 ∈ Fin) |
57 | 56 | ad2antrl 725 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) → 𝑧 ∈ Fin) |
58 | 55 | simplbi 498 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) → 𝑧 ⊆ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡}) |
59 | 58 | ad2antrl 725 |
. . . . . . . . . . . 12
⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) → 𝑧 ⊆ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡}) |
60 | | ssrab 4006 |
. . . . . . . . . . . . 13
⊢ (𝑧 ⊆ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ↔ (𝑧 ⊆ 𝐵 ∧ ∀𝑤 ∈ 𝑧 ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡)) |
61 | 60 | simprbi 497 |
. . . . . . . . . . . 12
⊢ (𝑧 ⊆ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → ∀𝑤 ∈ 𝑧 ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡) |
62 | 59, 61 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) → ∀𝑤 ∈ 𝑧 ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡) |
63 | | sseq2 3947 |
. . . . . . . . . . . 12
⊢ (𝑡 = (𝑓‘𝑤) → (𝑤 ⊆ 𝑡 ↔ 𝑤 ⊆ (𝑓‘𝑤))) |
64 | 63 | ac6sfi 9058 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ Fin ∧ ∀𝑤 ∈ 𝑧 ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡) → ∃𝑓(𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) |
65 | 57, 62, 64 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) → ∃𝑓(𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) |
66 | | frn 6607 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝑧⟶𝑢 → ran 𝑓 ⊆ 𝑢) |
67 | 66 | ad2antrl 725 |
. . . . . . . . . . . 12
⊢
(((((𝐵 ∈
TopBases ∧ 𝑋 = ∪ 𝐵)
∧ (𝑢 ⊆
(topGen‘𝐵) ∧
𝑋 = ∪ 𝑢))
∧ (𝑧 ∈ (𝒫
{𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ran 𝑓 ⊆ 𝑢) |
68 | | ffn 6600 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝑧⟶𝑢 → 𝑓 Fn 𝑧) |
69 | | dffn4 6694 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 Fn 𝑧 ↔ 𝑓:𝑧–onto→ran 𝑓) |
70 | 68, 69 | sylib 217 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝑧⟶𝑢 → 𝑓:𝑧–onto→ran 𝑓) |
71 | 70 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤)) → 𝑓:𝑧–onto→ran 𝑓) |
72 | | fofi 9105 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ Fin ∧ 𝑓:𝑧–onto→ran 𝑓) → ran 𝑓 ∈ Fin) |
73 | 57, 71, 72 | syl2an 596 |
. . . . . . . . . . . 12
⊢
(((((𝐵 ∈
TopBases ∧ 𝑋 = ∪ 𝐵)
∧ (𝑢 ⊆
(topGen‘𝐵) ∧
𝑋 = ∪ 𝑢))
∧ (𝑧 ∈ (𝒫
{𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ran 𝑓 ∈ Fin) |
74 | | elfpw 9121 |
. . . . . . . . . . . 12
⊢ (ran
𝑓 ∈ (𝒫 𝑢 ∩ Fin) ↔ (ran 𝑓 ⊆ 𝑢 ∧ ran 𝑓 ∈ Fin)) |
75 | 67, 73, 74 | sylanbrc 583 |
. . . . . . . . . . 11
⊢
(((((𝐵 ∈
TopBases ∧ 𝑋 = ∪ 𝐵)
∧ (𝑢 ⊆
(topGen‘𝐵) ∧
𝑋 = ∪ 𝑢))
∧ (𝑧 ∈ (𝒫
{𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ran 𝑓 ∈ (𝒫 𝑢 ∩ Fin)) |
76 | | simplrr 775 |
. . . . . . . . . . . . 13
⊢
(((((𝐵 ∈
TopBases ∧ 𝑋 = ∪ 𝐵)
∧ (𝑢 ⊆
(topGen‘𝐵) ∧
𝑋 = ∪ 𝑢))
∧ (𝑧 ∈ (𝒫
{𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → 𝑋 = ∪ 𝑧) |
77 | | uniiun 4988 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑧 =
∪ 𝑤 ∈ 𝑧 𝑤 |
78 | | ss2iun 4942 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑤 ∈
𝑧 𝑤 ⊆ (𝑓‘𝑤) → ∪
𝑤 ∈ 𝑧 𝑤 ⊆ ∪
𝑤 ∈ 𝑧 (𝑓‘𝑤)) |
79 | 77, 78 | eqsstrid 3969 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑤 ∈
𝑧 𝑤 ⊆ (𝑓‘𝑤) → ∪ 𝑧 ⊆ ∪ 𝑤 ∈ 𝑧 (𝑓‘𝑤)) |
80 | 79 | ad2antll 726 |
. . . . . . . . . . . . . 14
⊢
(((((𝐵 ∈
TopBases ∧ 𝑋 = ∪ 𝐵)
∧ (𝑢 ⊆
(topGen‘𝐵) ∧
𝑋 = ∪ 𝑢))
∧ (𝑧 ∈ (𝒫
{𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ∪ 𝑧 ⊆ ∪ 𝑤 ∈ 𝑧 (𝑓‘𝑤)) |
81 | | fniunfv 7120 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 Fn 𝑧 → ∪
𝑤 ∈ 𝑧 (𝑓‘𝑤) = ∪ ran 𝑓) |
82 | 68, 81 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝑧⟶𝑢 → ∪
𝑤 ∈ 𝑧 (𝑓‘𝑤) = ∪ ran 𝑓) |
83 | 82 | ad2antrl 725 |
. . . . . . . . . . . . . 14
⊢
(((((𝐵 ∈
TopBases ∧ 𝑋 = ∪ 𝐵)
∧ (𝑢 ⊆
(topGen‘𝐵) ∧
𝑋 = ∪ 𝑢))
∧ (𝑧 ∈ (𝒫
{𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ∪ 𝑤 ∈ 𝑧 (𝑓‘𝑤) = ∪ ran 𝑓) |
84 | 80, 83 | sseqtrd 3961 |
. . . . . . . . . . . . 13
⊢
(((((𝐵 ∈
TopBases ∧ 𝑋 = ∪ 𝐵)
∧ (𝑢 ⊆
(topGen‘𝐵) ∧
𝑋 = ∪ 𝑢))
∧ (𝑧 ∈ (𝒫
{𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ∪ 𝑧 ⊆ ∪ ran 𝑓) |
85 | 76, 84 | eqsstrd 3959 |
. . . . . . . . . . . 12
⊢
(((((𝐵 ∈
TopBases ∧ 𝑋 = ∪ 𝐵)
∧ (𝑢 ⊆
(topGen‘𝐵) ∧
𝑋 = ∪ 𝑢))
∧ (𝑧 ∈ (𝒫
{𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → 𝑋 ⊆ ∪ ran
𝑓) |
86 | 67 | unissd 4849 |
. . . . . . . . . . . . 13
⊢
(((((𝐵 ∈
TopBases ∧ 𝑋 = ∪ 𝐵)
∧ (𝑢 ⊆
(topGen‘𝐵) ∧
𝑋 = ∪ 𝑢))
∧ (𝑧 ∈ (𝒫
{𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ∪ ran
𝑓 ⊆ ∪ 𝑢) |
87 | 20 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢
(((((𝐵 ∈
TopBases ∧ 𝑋 = ∪ 𝐵)
∧ (𝑢 ⊆
(topGen‘𝐵) ∧
𝑋 = ∪ 𝑢))
∧ (𝑧 ∈ (𝒫
{𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → 𝑋 = ∪ 𝑢) |
88 | 86, 87 | sseqtrrd 3962 |
. . . . . . . . . . . 12
⊢
(((((𝐵 ∈
TopBases ∧ 𝑋 = ∪ 𝐵)
∧ (𝑢 ⊆
(topGen‘𝐵) ∧
𝑋 = ∪ 𝑢))
∧ (𝑧 ∈ (𝒫
{𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ∪ ran
𝑓 ⊆ 𝑋) |
89 | 85, 88 | eqssd 3938 |
. . . . . . . . . . 11
⊢
(((((𝐵 ∈
TopBases ∧ 𝑋 = ∪ 𝐵)
∧ (𝑢 ⊆
(topGen‘𝐵) ∧
𝑋 = ∪ 𝑢))
∧ (𝑧 ∈ (𝒫
{𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → 𝑋 = ∪ ran 𝑓) |
90 | | unieq 4850 |
. . . . . . . . . . . 12
⊢ (𝑣 = ran 𝑓 → ∪ 𝑣 = ∪
ran 𝑓) |
91 | 90 | rspceeqv 3575 |
. . . . . . . . . . 11
⊢ ((ran
𝑓 ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ∪
ran 𝑓) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣) |
92 | 75, 89, 91 | syl2anc 584 |
. . . . . . . . . 10
⊢
(((((𝐵 ∈
TopBases ∧ 𝑋 = ∪ 𝐵)
∧ (𝑢 ⊆
(topGen‘𝐵) ∧
𝑋 = ∪ 𝑢))
∧ (𝑧 ∈ (𝒫
{𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣) |
93 | 65, 92 | exlimddv 1938 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣) |
94 | 93 | rexlimdvaa 3214 |
. . . . . . . 8
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → (∃𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin)𝑋 = ∪ 𝑧 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣)) |
95 | 54, 94 | syld 47 |
. . . . . . 7
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣)) |
96 | 95 | expr 457 |
. . . . . 6
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ 𝑢 ⊆ (topGen‘𝐵)) → (𝑋 = ∪ 𝑢 → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣))) |
97 | 96 | com23 86 |
. . . . 5
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → (𝑋 = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣))) |
98 | 19, 97 | sylan2 593 |
. . . 4
⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) ∧ 𝑢 ∈ 𝒫 (topGen‘𝐵)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → (𝑋 = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣))) |
99 | 98 | ralrimdva 3106 |
. . 3
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → ∀𝑢 ∈ 𝒫
(topGen‘𝐵)(𝑋 = ∪
𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣))) |
100 | | tgcl 22119 |
. . . . . 6
⊢ (𝐵 ∈ TopBases →
(topGen‘𝐵) ∈
Top) |
101 | 100 | adantr 481 |
. . . . 5
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) →
(topGen‘𝐵) ∈
Top) |
102 | 1 | iscmp 22539 |
. . . . . 6
⊢
((topGen‘𝐵)
∈ Comp ↔ ((topGen‘𝐵) ∈ Top ∧ ∀𝑢 ∈ 𝒫
(topGen‘𝐵)(∪ (topGen‘𝐵) = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑣))) |
103 | 102 | baib 536 |
. . . . 5
⊢
((topGen‘𝐵)
∈ Top → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑢 ∈ 𝒫
(topGen‘𝐵)(∪ (topGen‘𝐵) = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑣))) |
104 | 101, 103 | syl 17 |
. . . 4
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) →
((topGen‘𝐵) ∈
Comp ↔ ∀𝑢
∈ 𝒫 (topGen‘𝐵)(∪
(topGen‘𝐵) = ∪ 𝑢
→ ∃𝑣 ∈
(𝒫 𝑢 ∩
Fin)∪ (topGen‘𝐵) = ∪ 𝑣))) |
105 | 6 | eqeq1d 2740 |
. . . . . 6
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → (∪ (topGen‘𝐵) = ∪ 𝑢 ↔ 𝑋 = ∪ 𝑢)) |
106 | 6 | eqeq1d 2740 |
. . . . . . 7
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → (∪ (topGen‘𝐵) = ∪ 𝑣 ↔ 𝑋 = ∪ 𝑣)) |
107 | 106 | rexbidv 3226 |
. . . . . 6
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → (∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣)) |
108 | 105, 107 | imbi12d 345 |
. . . . 5
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → ((∪ (topGen‘𝐵) = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑣) ↔ (𝑋 = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣))) |
109 | 108 | ralbidv 3112 |
. . . 4
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → (∀𝑢 ∈ 𝒫
(topGen‘𝐵)(∪ (topGen‘𝐵) = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑣) ↔ ∀𝑢 ∈ 𝒫
(topGen‘𝐵)(𝑋 = ∪
𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣))) |
110 | 104, 109 | bitrd 278 |
. . 3
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) →
((topGen‘𝐵) ∈
Comp ↔ ∀𝑢
∈ 𝒫 (topGen‘𝐵)(𝑋 = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣))) |
111 | 99, 110 | sylibrd 258 |
. 2
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → (topGen‘𝐵) ∈ Comp)) |
112 | 18, 111 | impbid 211 |
1
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪
𝐵) →
((topGen‘𝐵) ∈
Comp ↔ ∀𝑦
∈ 𝒫 𝐵(𝑋 = ∪
𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |