Step | Hyp | Ref
| Expression |
1 | | ssun1 3738 |
. . . 4
⊢ 𝐵 ⊆ (𝐵 ∪ {∅}) |
2 | | undif1 3995 |
. . . 4
⊢ ((𝐵 ∖ {∅}) ∪
{∅}) = (𝐵 ∪
{∅}) |
3 | 1, 2 | sseqtr4i 3601 |
. . 3
⊢ 𝐵 ⊆ ((𝐵 ∖ {∅}) ∪
{∅}) |
4 | | snex 4835 |
. . . 4
⊢ {∅}
∈ V |
5 | | unexg 6857 |
. . . 4
⊢ (((𝐵 ∖ {∅}) ∈
TopBases ∧ {∅} ∈ V) → ((𝐵 ∖ {∅}) ∪ {∅}) ∈
V) |
6 | 4, 5 | mpan2 703 |
. . 3
⊢ ((𝐵 ∖ {∅}) ∈
TopBases → ((𝐵 ∖
{∅}) ∪ {∅}) ∈ V) |
7 | | ssexg 4732 |
. . 3
⊢ ((𝐵 ⊆ ((𝐵 ∖ {∅}) ∪ {∅}) ∧
((𝐵 ∖ {∅})
∪ {∅}) ∈ V) → 𝐵 ∈ V) |
8 | 3, 6, 7 | sylancr 694 |
. 2
⊢ ((𝐵 ∖ {∅}) ∈
TopBases → 𝐵 ∈
V) |
9 | | elex 3185 |
. 2
⊢ (𝐵 ∈ TopBases → 𝐵 ∈ V) |
10 | | indif1 3830 |
. . . . . . . . . . 11
⊢ ((𝐵 ∖ {∅}) ∩
𝒫 (𝑥 ∩ 𝑦)) = ((𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)) ∖ {∅}) |
11 | 10 | unieqi 4381 |
. . . . . . . . . 10
⊢ ∪ ((𝐵
∖ {∅}) ∩ 𝒫 (𝑥 ∩ 𝑦)) = ∪ ((𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)) ∖ {∅}) |
12 | | unidif0 4764 |
. . . . . . . . . 10
⊢ ∪ ((𝐵
∩ 𝒫 (𝑥 ∩
𝑦)) ∖ {∅}) =
∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)) |
13 | 11, 12 | eqtri 2632 |
. . . . . . . . 9
⊢ ∪ ((𝐵
∖ {∅}) ∩ 𝒫 (𝑥 ∩ 𝑦)) = ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)) |
14 | 13 | sseq2i 3593 |
. . . . . . . 8
⊢ ((𝑥 ∩ 𝑦) ⊆ ∪
((𝐵 ∖ {∅})
∩ 𝒫 (𝑥 ∩
𝑦)) ↔ (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
15 | 14 | ralbii 2963 |
. . . . . . 7
⊢
(∀𝑦 ∈
(𝐵 ∖ {∅})(𝑥 ∩ 𝑦) ⊆ ∪
((𝐵 ∖ {∅})
∩ 𝒫 (𝑥 ∩
𝑦)) ↔ ∀𝑦 ∈ (𝐵 ∖ {∅})(𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
16 | | inss2 3796 |
. . . . . . . . . 10
⊢ (𝑥 ∩ 𝑦) ⊆ 𝑦 |
17 | | inss2 3796 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∩ {∅}) ⊆
{∅} |
18 | 17 | sseli 3564 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐵 ∩ {∅}) → 𝑦 ∈ {∅}) |
19 | | elsni 4142 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ {∅} → 𝑦 = ∅) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝐵 ∩ {∅}) → 𝑦 = ∅) |
21 | | 0ss 3924 |
. . . . . . . . . . 11
⊢ ∅
⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)) |
22 | 20, 21 | syl6eqss 3618 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐵 ∩ {∅}) → 𝑦 ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
23 | 16, 22 | syl5ss 3579 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝐵 ∩ {∅}) → (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
24 | 23 | rgen 2906 |
. . . . . . . 8
⊢
∀𝑦 ∈
(𝐵 ∩ {∅})(𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)) |
25 | | ralunb 3756 |
. . . . . . . 8
⊢
(∀𝑦 ∈
((𝐵 ∩ {∅}) ∪
(𝐵 ∖
{∅}))(𝑥 ∩ 𝑦) ⊆ ∪ (𝐵
∩ 𝒫 (𝑥 ∩
𝑦)) ↔ (∀𝑦 ∈ (𝐵 ∩ {∅})(𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)) ∧ ∀𝑦 ∈ (𝐵 ∖ {∅})(𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)))) |
26 | 24, 25 | mpbiran 955 |
. . . . . . 7
⊢
(∀𝑦 ∈
((𝐵 ∩ {∅}) ∪
(𝐵 ∖
{∅}))(𝑥 ∩ 𝑦) ⊆ ∪ (𝐵
∩ 𝒫 (𝑥 ∩
𝑦)) ↔ ∀𝑦 ∈ (𝐵 ∖ {∅})(𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
27 | | inundif 3998 |
. . . . . . . 8
⊢ ((𝐵 ∩ {∅}) ∪ (𝐵 ∖ {∅})) = 𝐵 |
28 | 27 | raleqi 3119 |
. . . . . . 7
⊢
(∀𝑦 ∈
((𝐵 ∩ {∅}) ∪
(𝐵 ∖
{∅}))(𝑥 ∩ 𝑦) ⊆ ∪ (𝐵
∩ 𝒫 (𝑥 ∩
𝑦)) ↔ ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
29 | 15, 26, 28 | 3bitr2i 287 |
. . . . . 6
⊢
(∀𝑦 ∈
(𝐵 ∖ {∅})(𝑥 ∩ 𝑦) ⊆ ∪
((𝐵 ∖ {∅})
∩ 𝒫 (𝑥 ∩
𝑦)) ↔ ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
30 | 29 | ralbii 2963 |
. . . . 5
⊢
(∀𝑥 ∈
(𝐵 ∖
{∅})∀𝑦 ∈
(𝐵 ∖ {∅})(𝑥 ∩ 𝑦) ⊆ ∪
((𝐵 ∖ {∅})
∩ 𝒫 (𝑥 ∩
𝑦)) ↔ ∀𝑥 ∈ (𝐵 ∖ {∅})∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
31 | | inss1 3795 |
. . . . . . . . 9
⊢ (𝑥 ∩ 𝑦) ⊆ 𝑥 |
32 | 17 | sseli 3564 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐵 ∩ {∅}) → 𝑥 ∈ {∅}) |
33 | | elsni 4142 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {∅} → 𝑥 = ∅) |
34 | 32, 33 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐵 ∩ {∅}) → 𝑥 = ∅) |
35 | 34, 21 | syl6eqss 3618 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ∩ {∅}) → 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
36 | 31, 35 | syl5ss 3579 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ∩ {∅}) → (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
37 | 36 | ralrimivw 2950 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐵 ∩ {∅}) → ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
38 | 37 | rgen 2906 |
. . . . . 6
⊢
∀𝑥 ∈
(𝐵 ∩
{∅})∀𝑦 ∈
𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)) |
39 | | ralunb 3756 |
. . . . . 6
⊢
(∀𝑥 ∈
((𝐵 ∩ {∅}) ∪
(𝐵 ∖
{∅}))∀𝑦 ∈
𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)) ↔ (∀𝑥 ∈ (𝐵 ∩ {∅})∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)) ∧ ∀𝑥 ∈ (𝐵 ∖ {∅})∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)))) |
40 | 38, 39 | mpbiran 955 |
. . . . 5
⊢
(∀𝑥 ∈
((𝐵 ∩ {∅}) ∪
(𝐵 ∖
{∅}))∀𝑦 ∈
𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)) ↔ ∀𝑥 ∈ (𝐵 ∖ {∅})∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
41 | 27 | raleqi 3119 |
. . . . 5
⊢
(∀𝑥 ∈
((𝐵 ∩ {∅}) ∪
(𝐵 ∖
{∅}))∀𝑦 ∈
𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
42 | 30, 40, 41 | 3bitr2i 287 |
. . . 4
⊢
(∀𝑥 ∈
(𝐵 ∖
{∅})∀𝑦 ∈
(𝐵 ∖ {∅})(𝑥 ∩ 𝑦) ⊆ ∪
((𝐵 ∖ {∅})
∩ 𝒫 (𝑥 ∩
𝑦)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
43 | 42 | a1i 11 |
. . 3
⊢ (𝐵 ∈ V → (∀𝑥 ∈ (𝐵 ∖ {∅})∀𝑦 ∈ (𝐵 ∖ {∅})(𝑥 ∩ 𝑦) ⊆ ∪
((𝐵 ∖ {∅})
∩ 𝒫 (𝑥 ∩
𝑦)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)))) |
44 | | difexg 4735 |
. . . 4
⊢ (𝐵 ∈ V → (𝐵 ∖ {∅}) ∈
V) |
45 | | isbasisg 20562 |
. . . 4
⊢ ((𝐵 ∖ {∅}) ∈ V
→ ((𝐵 ∖
{∅}) ∈ TopBases ↔ ∀𝑥 ∈ (𝐵 ∖ {∅})∀𝑦 ∈ (𝐵 ∖ {∅})(𝑥 ∩ 𝑦) ⊆ ∪
((𝐵 ∖ {∅})
∩ 𝒫 (𝑥 ∩
𝑦)))) |
46 | 44, 45 | syl 17 |
. . 3
⊢ (𝐵 ∈ V → ((𝐵 ∖ {∅}) ∈
TopBases ↔ ∀𝑥
∈ (𝐵 ∖
{∅})∀𝑦 ∈
(𝐵 ∖ {∅})(𝑥 ∩ 𝑦) ⊆ ∪
((𝐵 ∖ {∅})
∩ 𝒫 (𝑥 ∩
𝑦)))) |
47 | | isbasisg 20562 |
. . 3
⊢ (𝐵 ∈ V → (𝐵 ∈ TopBases ↔
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)))) |
48 | 43, 46, 47 | 3bitr4d 299 |
. 2
⊢ (𝐵 ∈ V → ((𝐵 ∖ {∅}) ∈
TopBases ↔ 𝐵 ∈
TopBases)) |
49 | 8, 9, 48 | pm5.21nii 367 |
1
⊢ ((𝐵 ∖ {∅}) ∈
TopBases ↔ 𝐵 ∈
TopBases) |