Step | Hyp | Ref
| Expression |
1 | | uniss 4458 |
. . . . . . . 8
⊢ (𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢
⊆ ∪ (topGen‘𝐵)) |
2 | 1 | adantl 482 |
. . . . . . 7
⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∪ 𝑢
⊆ ∪ (topGen‘𝐵)) |
3 | | unitg 20771 |
. . . . . . . 8
⊢ (𝐵 ∈ TopBases → ∪ (topGen‘𝐵) = ∪ 𝐵) |
4 | 3 | adantr 481 |
. . . . . . 7
⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∪ (topGen‘𝐵) = ∪ 𝐵) |
5 | 2, 4 | sseqtrd 3641 |
. . . . . 6
⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∪ 𝑢
⊆ ∪ 𝐵) |
6 | | eluni2 4440 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑢
↔ ∃𝑡 ∈
𝑢 𝑥 ∈ 𝑡) |
7 | | ssel2 3598 |
. . . . . . . . . . . 12
⊢ ((𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ (topGen‘𝐵)) |
8 | | eltg2b 20763 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) ↔ ∀𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))) |
9 | | rsp 2929 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
𝑡 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → (𝑥 ∈ 𝑡 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡))) |
10 | 8, 9 | syl6bi 243 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ TopBases → (𝑡 ∈ (topGen‘𝐵) → (𝑥 ∈ 𝑡 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡)))) |
11 | 10 | imp31 448 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ TopBases ∧ 𝑡 ∈ (topGen‘𝐵)) ∧ 𝑥 ∈ 𝑡) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡)) |
12 | 11 | an32s 846 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ TopBases ∧ 𝑥 ∈ 𝑡) ∧ 𝑡 ∈ (topGen‘𝐵)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡)) |
13 | 7, 12 | sylan2 491 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ TopBases ∧ 𝑥 ∈ 𝑡) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑡 ∈ 𝑢)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡)) |
14 | 13 | an42s 870 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡)) |
15 | | elssuni 4467 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ 𝑢 → 𝑡 ⊆ ∪ 𝑢) |
16 | | sstr2 3610 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ⊆ 𝑡 → (𝑡 ⊆ ∪ 𝑢 → 𝑦 ⊆ ∪ 𝑢)) |
17 | 15, 16 | syl5com 31 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝑢 → (𝑦 ⊆ 𝑡 → 𝑦 ⊆ ∪ 𝑢)) |
18 | 17 | anim2d 589 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ 𝑢 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))) |
19 | 18 | reximdv 3016 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ 𝑢 → (∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))) |
20 | 19 | ad2antrl 764 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡)) → (∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))) |
21 | 14, 20 | mpd 15 |
. . . . . . . . 9
⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)) |
22 | 21 | rexlimdvaa 3032 |
. . . . . . . 8
⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∃𝑡 ∈ 𝑢 𝑥 ∈ 𝑡 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))) |
23 | 6, 22 | syl5bi 232 |
. . . . . . 7
⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (𝑥 ∈ ∪ 𝑢 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))) |
24 | 23 | ralrimiv 2965 |
. . . . . 6
⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)) |
25 | 5, 24 | jca 554 |
. . . . 5
⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∪ 𝑢
⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢))) |
26 | 25 | ex 450 |
. . . 4
⊢ (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → (∪ 𝑢
⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))) |
27 | | eltg2 20762 |
. . . 4
⊢ (𝐵 ∈ TopBases → (∪ 𝑢
∈ (topGen‘𝐵)
↔ (∪ 𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝑢∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢)))) |
28 | 26, 27 | sylibrd 249 |
. . 3
⊢ (𝐵 ∈ TopBases → (𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢
∈ (topGen‘𝐵))) |
29 | 28 | alrimiv 1855 |
. 2
⊢ (𝐵 ∈ TopBases →
∀𝑢(𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢
∈ (topGen‘𝐵))) |
30 | | inss1 3833 |
. . . . . . . 8
⊢ (𝑢 ∩ 𝑣) ⊆ 𝑢 |
31 | | tg1 20768 |
. . . . . . . 8
⊢ (𝑢 ∈ (topGen‘𝐵) → 𝑢 ⊆ ∪ 𝐵) |
32 | 30, 31 | syl5ss 3614 |
. . . . . . 7
⊢ (𝑢 ∈ (topGen‘𝐵) → (𝑢 ∩ 𝑣) ⊆ ∪ 𝐵) |
33 | 32 | ad2antrl 764 |
. . . . . 6
⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑢 ∩ 𝑣) ⊆ ∪ 𝐵) |
34 | | eltg2 20762 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ TopBases → (𝑢 ∈ (topGen‘𝐵) ↔ (𝑢 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝑢 ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢)))) |
35 | 34 | simplbda 654 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → ∀𝑥 ∈ 𝑢 ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢)) |
36 | | rsp 2929 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝑢 ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) → (𝑥 ∈ 𝑢 → ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢))) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) → (𝑥 ∈ 𝑢 → ∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢))) |
38 | | eltg2 20762 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ TopBases → (𝑣 ∈ (topGen‘𝐵) ↔ (𝑣 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝑣 ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))) |
39 | 38 | simplbda 654 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → ∀𝑥 ∈ 𝑣 ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) |
40 | | rsp 2929 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝑣 ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣) → (𝑥 ∈ 𝑣 → ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑥 ∈ 𝑣 → ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))) |
42 | 37, 41 | im2anan9 880 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣) → (∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))) |
43 | | elin 3796 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑢 ∩ 𝑣) ↔ (𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣)) |
44 | | reeanv 3107 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) ↔ (∃𝑧 ∈ 𝐵 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ ∃𝑤 ∈ 𝐵 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))) |
45 | 42, 43, 44 | 3imtr4g 285 |
. . . . . . . . 9
⊢ (((𝐵 ∈ TopBases ∧ 𝑢 ∈ (topGen‘𝐵)) ∧ (𝐵 ∈ TopBases ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))) |
46 | 45 | anandis 873 |
. . . . . . . 8
⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))) |
47 | | elin 3796 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝑧 ∩ 𝑤) ↔ (𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤)) |
48 | 47 | biimpri 218 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑥 ∈ (𝑧 ∩ 𝑤)) |
49 | | ss2in 3840 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)) |
50 | 48, 49 | anim12i 590 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) ∧ (𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣)) → (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣))) |
51 | 50 | an4s 869 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣))) |
52 | | basis2 20755 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ TopBases ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ 𝑥 ∈ (𝑧 ∩ 𝑤))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤))) |
53 | 52 | adantllr 755 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ 𝑥 ∈ (𝑧 ∩ 𝑤))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤))) |
54 | 53 | adantrrr 761 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤))) |
55 | | sstr2 3610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ⊆ (𝑧 ∩ 𝑤) → ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → 𝑡 ⊆ (𝑢 ∩ 𝑣))) |
56 | 55 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (𝑡 ⊆ (𝑧 ∩ 𝑤) → 𝑡 ⊆ (𝑢 ∩ 𝑣))) |
57 | 56 | anim2d 589 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → ((𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))) |
58 | 57 | reximdv 3016 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))) |
59 | 58 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)) → (∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))) |
60 | 59 | ad2antll 765 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))) → (∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑧 ∩ 𝑤)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))) |
61 | 54, 60 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ (𝑥 ∈ (𝑧 ∩ 𝑤) ∧ (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))) |
62 | 51, 61 | sylanr2 685 |
. . . . . . . . . . . . 13
⊢ ((((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) ∧ (𝑤 ∈ 𝐵 ∧ ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))) |
63 | 62 | rexlimdvaa 3032 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐵) → (∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))) |
64 | 63 | rexlimdva 3031 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ TopBases ∧ 𝑥 ∈ (𝑢 ∩ 𝑣)) → (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))) |
65 | 64 | ex 450 |
. . . . . . . . . 10
⊢ (𝐵 ∈ TopBases → (𝑥 ∈ (𝑢 ∩ 𝑣) → (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))) |
66 | 65 | a2d 29 |
. . . . . . . . 9
⊢ (𝐵 ∈ TopBases → ((𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))) |
67 | 66 | imp 445 |
. . . . . . . 8
⊢ ((𝐵 ∈ TopBases ∧ (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 ((𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣)))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))) |
68 | 46, 67 | syldan 487 |
. . . . . . 7
⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → (𝑥 ∈ (𝑢 ∩ 𝑣) → ∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))) |
69 | 68 | ralrimiv 2965 |
. . . . . 6
⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))) |
70 | 33, 69 | jca 554 |
. . . . 5
⊢ ((𝐵 ∈ TopBases ∧ (𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵))) → ((𝑢 ∩ 𝑣) ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))) |
71 | 70 | ex 450 |
. . . 4
⊢ (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → ((𝑢 ∩ 𝑣) ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))) |
72 | | eltg2 20762 |
. . . 4
⊢ (𝐵 ∈ TopBases → ((𝑢 ∩ 𝑣) ∈ (topGen‘𝐵) ↔ ((𝑢 ∩ 𝑣) ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))))) |
73 | 71, 72 | sylibrd 249 |
. . 3
⊢ (𝐵 ∈ TopBases → ((𝑢 ∈ (topGen‘𝐵) ∧ 𝑣 ∈ (topGen‘𝐵)) → (𝑢 ∩ 𝑣) ∈ (topGen‘𝐵))) |
74 | 73 | ralrimivv 2970 |
. 2
⊢ (𝐵 ∈ TopBases →
∀𝑢 ∈
(topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢 ∩ 𝑣) ∈ (topGen‘𝐵)) |
75 | | fvex 6201 |
. . 3
⊢
(topGen‘𝐵)
∈ V |
76 | | istopg 20700 |
. . 3
⊢
((topGen‘𝐵)
∈ V → ((topGen‘𝐵) ∈ Top ↔ (∀𝑢(𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ∈ (topGen‘𝐵)) ∧ ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢 ∩ 𝑣) ∈ (topGen‘𝐵)))) |
77 | 75, 76 | ax-mp 5 |
. 2
⊢
((topGen‘𝐵)
∈ Top ↔ (∀𝑢(𝑢 ⊆ (topGen‘𝐵) → ∪ 𝑢 ∈ (topGen‘𝐵)) ∧ ∀𝑢 ∈ (topGen‘𝐵)∀𝑣 ∈ (topGen‘𝐵)(𝑢 ∩ 𝑣) ∈ (topGen‘𝐵))) |
78 | 29, 74, 77 | sylanbrc 698 |
1
⊢ (𝐵 ∈ TopBases →
(topGen‘𝐵) ∈
Top) |