Step | Hyp | Ref
| Expression |
1 | | toponuni 20719 |
. . . . . 6
⊢ (𝑏 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝑏) |
2 | | eqimss2 3658 |
. . . . . . 7
⊢ (𝐵 = ∪
𝑏 → ∪ 𝑏
⊆ 𝐵) |
3 | | sspwuni 4611 |
. . . . . . 7
⊢ (𝑏 ⊆ 𝒫 𝐵 ↔ ∪ 𝑏
⊆ 𝐵) |
4 | 2, 3 | sylibr 224 |
. . . . . 6
⊢ (𝐵 = ∪
𝑏 → 𝑏 ⊆ 𝒫 𝐵) |
5 | 1, 4 | syl 17 |
. . . . 5
⊢ (𝑏 ∈ (TopOn‘𝐵) → 𝑏 ⊆ 𝒫 𝐵) |
6 | | selpw 4165 |
. . . . 5
⊢ (𝑏 ∈ 𝒫 𝒫
𝐵 ↔ 𝑏 ⊆ 𝒫 𝐵) |
7 | 5, 6 | sylibr 224 |
. . . 4
⊢ (𝑏 ∈ (TopOn‘𝐵) → 𝑏 ∈ 𝒫 𝒫 𝐵) |
8 | 7 | ssriv 3607 |
. . 3
⊢
(TopOn‘𝐵)
⊆ 𝒫 𝒫 𝐵 |
9 | 8 | a1i 11 |
. 2
⊢ (𝐵 ∈ 𝑉 → (TopOn‘𝐵) ⊆ 𝒫 𝒫 𝐵) |
10 | | distopon 20801 |
. 2
⊢ (𝐵 ∈ 𝑉 → 𝒫 𝐵 ∈ (TopOn‘𝐵)) |
11 | | simpl 473 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → 𝑏 ⊆ (TopOn‘𝐵)) |
12 | 11 | sselda 3603 |
. . . . . . . . . . . . 13
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑥 ∈ 𝑏) → 𝑥 ∈ (TopOn‘𝐵)) |
13 | 12 | adantrl 752 |
. . . . . . . . . . . 12
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ⊆ ∩ 𝑏 ∧ 𝑥 ∈ 𝑏)) → 𝑥 ∈ (TopOn‘𝐵)) |
14 | | topontop 20718 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (TopOn‘𝐵) → 𝑥 ∈ Top) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ⊆ ∩ 𝑏 ∧ 𝑥 ∈ 𝑏)) → 𝑥 ∈ Top) |
16 | | simpl 473 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ⊆ ∩ 𝑏
∧ 𝑥 ∈ 𝑏) → 𝑐 ⊆ ∩ 𝑏) |
17 | | intss1 4492 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑏 → ∩ 𝑏 ⊆ 𝑥) |
18 | 17 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ⊆ ∩ 𝑏
∧ 𝑥 ∈ 𝑏) → ∩ 𝑏
⊆ 𝑥) |
19 | 16, 18 | sstrd 3613 |
. . . . . . . . . . . 12
⊢ ((𝑐 ⊆ ∩ 𝑏
∧ 𝑥 ∈ 𝑏) → 𝑐 ⊆ 𝑥) |
20 | 19 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ⊆ ∩ 𝑏 ∧ 𝑥 ∈ 𝑏)) → 𝑐 ⊆ 𝑥) |
21 | | uniopn 20702 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ Top ∧ 𝑐 ⊆ 𝑥) → ∪ 𝑐 ∈ 𝑥) |
22 | 15, 20, 21 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ⊆ ∩ 𝑏 ∧ 𝑥 ∈ 𝑏)) → ∪ 𝑐 ∈ 𝑥) |
23 | 22 | expr 643 |
. . . . . . . . 9
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 ⊆ ∩ 𝑏) → (𝑥 ∈ 𝑏 → ∪ 𝑐 ∈ 𝑥)) |
24 | 23 | ralrimiv 2965 |
. . . . . . . 8
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 ⊆ ∩ 𝑏) → ∀𝑥 ∈ 𝑏 ∪ 𝑐 ∈ 𝑥) |
25 | | vuniex 6954 |
. . . . . . . . 9
⊢ ∪ 𝑐
∈ V |
26 | 25 | elint2 4482 |
. . . . . . . 8
⊢ (∪ 𝑐
∈ ∩ 𝑏 ↔ ∀𝑥 ∈ 𝑏 ∪ 𝑐 ∈ 𝑥) |
27 | 24, 26 | sylibr 224 |
. . . . . . 7
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 ⊆ ∩ 𝑏) → ∪ 𝑐
∈ ∩ 𝑏) |
28 | 27 | ex 450 |
. . . . . 6
⊢ ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → (𝑐 ⊆ ∩ 𝑏 → ∪ 𝑐
∈ ∩ 𝑏)) |
29 | 28 | alrimiv 1855 |
. . . . 5
⊢ ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∀𝑐(𝑐 ⊆ ∩ 𝑏 → ∪ 𝑐
∈ ∩ 𝑏)) |
30 | | simpll 790 |
. . . . . . . . . . 11
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ∈ ∩ 𝑏 ∧ 𝑥 ∈ ∩ 𝑏)) → 𝑏 ⊆ (TopOn‘𝐵)) |
31 | 30 | sselda 3603 |
. . . . . . . . . 10
⊢ ((((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ∈ ∩ 𝑏 ∧ 𝑥 ∈ ∩ 𝑏)) ∧ 𝑦 ∈ 𝑏) → 𝑦 ∈ (TopOn‘𝐵)) |
32 | | topontop 20718 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (TopOn‘𝐵) → 𝑦 ∈ Top) |
33 | 31, 32 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ∈ ∩ 𝑏 ∧ 𝑥 ∈ ∩ 𝑏)) ∧ 𝑦 ∈ 𝑏) → 𝑦 ∈ Top) |
34 | | intss1 4492 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑏 → ∩ 𝑏 ⊆ 𝑦) |
35 | 34 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ∈ ∩ 𝑏 ∧ 𝑥 ∈ ∩ 𝑏)) ∧ 𝑦 ∈ 𝑏) → ∩ 𝑏 ⊆ 𝑦) |
36 | | simplrl 800 |
. . . . . . . . . 10
⊢ ((((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ∈ ∩ 𝑏 ∧ 𝑥 ∈ ∩ 𝑏)) ∧ 𝑦 ∈ 𝑏) → 𝑐 ∈ ∩ 𝑏) |
37 | 35, 36 | sseldd 3604 |
. . . . . . . . 9
⊢ ((((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ∈ ∩ 𝑏 ∧ 𝑥 ∈ ∩ 𝑏)) ∧ 𝑦 ∈ 𝑏) → 𝑐 ∈ 𝑦) |
38 | | simplrr 801 |
. . . . . . . . . 10
⊢ ((((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ∈ ∩ 𝑏 ∧ 𝑥 ∈ ∩ 𝑏)) ∧ 𝑦 ∈ 𝑏) → 𝑥 ∈ ∩ 𝑏) |
39 | 35, 38 | sseldd 3604 |
. . . . . . . . 9
⊢ ((((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ∈ ∩ 𝑏 ∧ 𝑥 ∈ ∩ 𝑏)) ∧ 𝑦 ∈ 𝑏) → 𝑥 ∈ 𝑦) |
40 | | inopn 20704 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Top ∧ 𝑐 ∈ 𝑦 ∧ 𝑥 ∈ 𝑦) → (𝑐 ∩ 𝑥) ∈ 𝑦) |
41 | 33, 37, 39, 40 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ∈ ∩ 𝑏 ∧ 𝑥 ∈ ∩ 𝑏)) ∧ 𝑦 ∈ 𝑏) → (𝑐 ∩ 𝑥) ∈ 𝑦) |
42 | 41 | ralrimiva 2966 |
. . . . . . 7
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ∈ ∩ 𝑏 ∧ 𝑥 ∈ ∩ 𝑏)) → ∀𝑦 ∈ 𝑏 (𝑐 ∩ 𝑥) ∈ 𝑦) |
43 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑐 ∈ V |
44 | 43 | inex1 4799 |
. . . . . . . 8
⊢ (𝑐 ∩ 𝑥) ∈ V |
45 | 44 | elint2 4482 |
. . . . . . 7
⊢ ((𝑐 ∩ 𝑥) ∈ ∩ 𝑏 ↔ ∀𝑦 ∈ 𝑏 (𝑐 ∩ 𝑥) ∈ 𝑦) |
46 | 42, 45 | sylibr 224 |
. . . . . 6
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ∈ ∩ 𝑏 ∧ 𝑥 ∈ ∩ 𝑏)) → (𝑐 ∩ 𝑥) ∈ ∩ 𝑏) |
47 | 46 | ralrimivva 2971 |
. . . . 5
⊢ ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∀𝑐 ∈ ∩ 𝑏∀𝑥 ∈ ∩ 𝑏(𝑐 ∩ 𝑥) ∈ ∩ 𝑏) |
48 | | intex 4820 |
. . . . . . . 8
⊢ (𝑏 ≠ ∅ ↔ ∩ 𝑏
∈ V) |
49 | 48 | biimpi 206 |
. . . . . . 7
⊢ (𝑏 ≠ ∅ → ∩ 𝑏
∈ V) |
50 | 49 | adantl 482 |
. . . . . 6
⊢ ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∩ 𝑏
∈ V) |
51 | | istopg 20700 |
. . . . . 6
⊢ (∩ 𝑏
∈ V → (∩ 𝑏 ∈ Top ↔ (∀𝑐(𝑐 ⊆ ∩ 𝑏 → ∪ 𝑐
∈ ∩ 𝑏) ∧ ∀𝑐 ∈ ∩ 𝑏∀𝑥 ∈ ∩ 𝑏(𝑐 ∩ 𝑥) ∈ ∩ 𝑏))) |
52 | 50, 51 | syl 17 |
. . . . 5
⊢ ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → (∩ 𝑏
∈ Top ↔ (∀𝑐(𝑐 ⊆ ∩ 𝑏 → ∪ 𝑐
∈ ∩ 𝑏) ∧ ∀𝑐 ∈ ∩ 𝑏∀𝑥 ∈ ∩ 𝑏(𝑐 ∩ 𝑥) ∈ ∩ 𝑏))) |
53 | 29, 47, 52 | mpbir2and 957 |
. . . 4
⊢ ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∩ 𝑏
∈ Top) |
54 | 53 | 3adant1 1079 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∩ 𝑏
∈ Top) |
55 | | n0 3931 |
. . . . . . . . . . 11
⊢ (𝑏 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝑏) |
56 | 55 | biimpi 206 |
. . . . . . . . . 10
⊢ (𝑏 ≠ ∅ →
∃𝑥 𝑥 ∈ 𝑏) |
57 | 56 | ad2antlr 763 |
. . . . . . . . 9
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ ∩ 𝑏) → ∃𝑥 𝑥 ∈ 𝑏) |
58 | 17 | sselda 3603 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑏 ∧ 𝑐 ∈ ∩ 𝑏) → 𝑐 ∈ 𝑥) |
59 | 58 | ancoms 469 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ ∩ 𝑏
∧ 𝑥 ∈ 𝑏) → 𝑐 ∈ 𝑥) |
60 | | elssuni 4467 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ 𝑥 → 𝑐 ⊆ ∪ 𝑥) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ ∩ 𝑏
∧ 𝑥 ∈ 𝑏) → 𝑐 ⊆ ∪ 𝑥) |
62 | 61 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ∈ ∩ 𝑏 ∧ 𝑥 ∈ 𝑏)) → 𝑐 ⊆ ∪ 𝑥) |
63 | 12 | adantrl 752 |
. . . . . . . . . . . . 13
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ∈ ∩ 𝑏 ∧ 𝑥 ∈ 𝑏)) → 𝑥 ∈ (TopOn‘𝐵)) |
64 | | toponuni 20719 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝑥) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ∈ ∩ 𝑏 ∧ 𝑥 ∈ 𝑏)) → 𝐵 = ∪ 𝑥) |
66 | 62, 65 | sseqtr4d 3642 |
. . . . . . . . . . 11
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ (𝑐 ∈ ∩ 𝑏 ∧ 𝑥 ∈ 𝑏)) → 𝑐 ⊆ 𝐵) |
67 | 66 | expr 643 |
. . . . . . . . . 10
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ ∩ 𝑏) → (𝑥 ∈ 𝑏 → 𝑐 ⊆ 𝐵)) |
68 | 67 | exlimdv 1861 |
. . . . . . . . 9
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ ∩ 𝑏) → (∃𝑥 𝑥 ∈ 𝑏 → 𝑐 ⊆ 𝐵)) |
69 | 57, 68 | mpd 15 |
. . . . . . . 8
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ ∩ 𝑏) → 𝑐 ⊆ 𝐵) |
70 | 69 | ralrimiva 2966 |
. . . . . . 7
⊢ ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∀𝑐 ∈ ∩ 𝑏𝑐 ⊆ 𝐵) |
71 | | unissb 4469 |
. . . . . . 7
⊢ (∪ ∩ 𝑏 ⊆ 𝐵 ↔ ∀𝑐 ∈ ∩ 𝑏𝑐 ⊆ 𝐵) |
72 | 70, 71 | sylibr 224 |
. . . . . 6
⊢ ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∪ ∩ 𝑏 ⊆ 𝐵) |
73 | 72 | 3adant1 1079 |
. . . . 5
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∪ ∩ 𝑏 ⊆ 𝐵) |
74 | 11 | sselda 3603 |
. . . . . . . . . 10
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ 𝑏) → 𝑐 ∈ (TopOn‘𝐵)) |
75 | | toponuni 20719 |
. . . . . . . . . 10
⊢ (𝑐 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝑐) |
76 | 74, 75 | syl 17 |
. . . . . . . . 9
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ 𝑏) → 𝐵 = ∪ 𝑐) |
77 | | topontop 20718 |
. . . . . . . . . 10
⊢ (𝑐 ∈ (TopOn‘𝐵) → 𝑐 ∈ Top) |
78 | | eqid 2622 |
. . . . . . . . . . 11
⊢ ∪ 𝑐 =
∪ 𝑐 |
79 | 78 | topopn 20711 |
. . . . . . . . . 10
⊢ (𝑐 ∈ Top → ∪ 𝑐
∈ 𝑐) |
80 | 74, 77, 79 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ 𝑏) → ∪ 𝑐 ∈ 𝑐) |
81 | 76, 80 | eqeltrd 2701 |
. . . . . . . 8
⊢ (((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ 𝑏) → 𝐵 ∈ 𝑐) |
82 | 81 | ralrimiva 2966 |
. . . . . . 7
⊢ ((𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∀𝑐 ∈ 𝑏 𝐵 ∈ 𝑐) |
83 | 82 | 3adant1 1079 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∀𝑐 ∈ 𝑏 𝐵 ∈ 𝑐) |
84 | | elintg 4483 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ ∩ 𝑏 ↔ ∀𝑐 ∈ 𝑏 𝐵 ∈ 𝑐)) |
85 | 84 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → (𝐵 ∈ ∩ 𝑏 ↔ ∀𝑐 ∈ 𝑏 𝐵 ∈ 𝑐)) |
86 | 83, 85 | mpbird 247 |
. . . . 5
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → 𝐵 ∈ ∩ 𝑏) |
87 | | unissel 4468 |
. . . . 5
⊢ ((∪ ∩ 𝑏 ⊆ 𝐵 ∧ 𝐵 ∈ ∩ 𝑏) → ∪ ∩ 𝑏 = 𝐵) |
88 | 73, 86, 87 | syl2anc 693 |
. . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∪ ∩ 𝑏 = 𝐵) |
89 | 88 | eqcomd 2628 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → 𝐵 = ∪ ∩ 𝑏) |
90 | | istopon 20717 |
. . 3
⊢ (∩ 𝑏
∈ (TopOn‘𝐵)
↔ (∩ 𝑏 ∈ Top ∧ 𝐵 = ∪ ∩ 𝑏)) |
91 | 54, 89, 90 | sylanbrc 698 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑏 ⊆ (TopOn‘𝐵) ∧ 𝑏 ≠ ∅) → ∩ 𝑏
∈ (TopOn‘𝐵)) |
92 | 9, 10, 91 | ismred 16262 |
1
⊢ (𝐵 ∈ 𝑉 → (TopOn‘𝐵) ∈ (Moore‘𝒫 𝐵)) |