Step | Hyp | Ref
| Expression |
1 | | ssrab2 4014 |
. . . 4
⊢ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ⊆ 𝐽 |
2 | | opnfbas.1 |
. . . . . 6
⊢ 𝑋 = ∪
𝐽 |
3 | 2 | eqimss2i 3981 |
. . . . 5
⊢ ∪ 𝐽
⊆ 𝑋 |
4 | | sspwuni 5031 |
. . . . 5
⊢ (𝐽 ⊆ 𝒫 𝑋 ↔ ∪ 𝐽
⊆ 𝑋) |
5 | 3, 4 | mpbir 230 |
. . . 4
⊢ 𝐽 ⊆ 𝒫 𝑋 |
6 | 1, 5 | sstri 3931 |
. . 3
⊢ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ⊆ 𝒫 𝑋 |
7 | 6 | a1i 11 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ⊆ 𝒫 𝑋) |
8 | 2 | topopn 22053 |
. . . . . . 7
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
9 | 8 | anim1i 615 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑋 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋)) |
10 | 9 | 3adant3 1131 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑋 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋)) |
11 | | sseq2 3948 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑋)) |
12 | 11 | elrab 3625 |
. . . . 5
⊢ (𝑋 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ↔ (𝑋 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋)) |
13 | 10, 12 | sylibr 233 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → 𝑋 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}) |
14 | 13 | ne0d 4271 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ≠ ∅) |
15 | | ss0 4334 |
. . . . . . 7
⊢ (𝑆 ⊆ ∅ → 𝑆 = ∅) |
16 | 15 | necon3ai 2968 |
. . . . . 6
⊢ (𝑆 ≠ ∅ → ¬ 𝑆 ⊆
∅) |
17 | 16 | 3ad2ant3 1134 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ¬ 𝑆 ⊆
∅) |
18 | 17 | intnand 489 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ¬ (∅ ∈
𝐽 ∧ 𝑆 ⊆ ∅)) |
19 | | df-nel 3050 |
. . . . 5
⊢ (∅
∉ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ↔ ¬ ∅ ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}) |
20 | | sseq2 3948 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ ∅)) |
21 | 20 | elrab 3625 |
. . . . . 6
⊢ (∅
∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ↔ (∅ ∈ 𝐽 ∧ 𝑆 ⊆ ∅)) |
22 | 21 | notbii 320 |
. . . . 5
⊢ (¬
∅ ∈ {𝑥 ∈
𝐽 ∣ 𝑆 ⊆ 𝑥} ↔ ¬ (∅ ∈ 𝐽 ∧ 𝑆 ⊆ ∅)) |
23 | 19, 22 | bitr2i 275 |
. . . 4
⊢ (¬
(∅ ∈ 𝐽 ∧
𝑆 ⊆ ∅) ↔
∅ ∉ {𝑥 ∈
𝐽 ∣ 𝑆 ⊆ 𝑥}) |
24 | 18, 23 | sylib 217 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ∅ ∉ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}) |
25 | | sseq2 3948 |
. . . . . . 7
⊢ (𝑥 = 𝑟 → (𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑟)) |
26 | 25 | elrab 3625 |
. . . . . 6
⊢ (𝑟 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ↔ (𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟)) |
27 | | sseq2 3948 |
. . . . . . 7
⊢ (𝑥 = 𝑠 → (𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑠)) |
28 | 27 | elrab 3625 |
. . . . . 6
⊢ (𝑠 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ↔ (𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠)) |
29 | 26, 28 | anbi12i 627 |
. . . . 5
⊢ ((𝑟 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∧ 𝑠 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}) ↔ ((𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟) ∧ (𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠))) |
30 | | simpl 483 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ ((𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟) ∧ (𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠))) → 𝐽 ∈ Top) |
31 | | simprll 776 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ ((𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟) ∧ (𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠))) → 𝑟 ∈ 𝐽) |
32 | | simprrl 778 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ ((𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟) ∧ (𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠))) → 𝑠 ∈ 𝐽) |
33 | | inopn 22046 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽) → (𝑟 ∩ 𝑠) ∈ 𝐽) |
34 | 30, 31, 32, 33 | syl3anc 1370 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ ((𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟) ∧ (𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠))) → (𝑟 ∩ 𝑠) ∈ 𝐽) |
35 | | ssin 4166 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ⊆ 𝑟 ∧ 𝑆 ⊆ 𝑠) ↔ 𝑆 ⊆ (𝑟 ∩ 𝑠)) |
36 | 35 | biimpi 215 |
. . . . . . . . . . . 12
⊢ ((𝑆 ⊆ 𝑟 ∧ 𝑆 ⊆ 𝑠) → 𝑆 ⊆ (𝑟 ∩ 𝑠)) |
37 | 36 | ad2ant2l 743 |
. . . . . . . . . . 11
⊢ (((𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟) ∧ (𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠)) → 𝑆 ⊆ (𝑟 ∩ 𝑠)) |
38 | 37 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ ((𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟) ∧ (𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠))) → 𝑆 ⊆ (𝑟 ∩ 𝑠)) |
39 | 34, 38 | jca 512 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ ((𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟) ∧ (𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠))) → ((𝑟 ∩ 𝑠) ∈ 𝐽 ∧ 𝑆 ⊆ (𝑟 ∩ 𝑠))) |
40 | 39 | 3ad2antl1 1184 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) ∧ ((𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟) ∧ (𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠))) → ((𝑟 ∩ 𝑠) ∈ 𝐽 ∧ 𝑆 ⊆ (𝑟 ∩ 𝑠))) |
41 | | sseq2 3948 |
. . . . . . . . 9
⊢ (𝑥 = (𝑟 ∩ 𝑠) → (𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ (𝑟 ∩ 𝑠))) |
42 | 41 | elrab 3625 |
. . . . . . . 8
⊢ ((𝑟 ∩ 𝑠) ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ↔ ((𝑟 ∩ 𝑠) ∈ 𝐽 ∧ 𝑆 ⊆ (𝑟 ∩ 𝑠))) |
43 | 40, 42 | sylibr 233 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) ∧ ((𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟) ∧ (𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠))) → (𝑟 ∩ 𝑠) ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}) |
44 | | ssid 3944 |
. . . . . . 7
⊢ (𝑟 ∩ 𝑠) ⊆ (𝑟 ∩ 𝑠) |
45 | | sseq1 3947 |
. . . . . . . 8
⊢ (𝑡 = (𝑟 ∩ 𝑠) → (𝑡 ⊆ (𝑟 ∩ 𝑠) ↔ (𝑟 ∩ 𝑠) ⊆ (𝑟 ∩ 𝑠))) |
46 | 45 | rspcev 3561 |
. . . . . . 7
⊢ (((𝑟 ∩ 𝑠) ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∧ (𝑟 ∩ 𝑠) ⊆ (𝑟 ∩ 𝑠)) → ∃𝑡 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}𝑡 ⊆ (𝑟 ∩ 𝑠)) |
47 | 43, 44, 46 | sylancl 586 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) ∧ ((𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟) ∧ (𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠))) → ∃𝑡 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}𝑡 ⊆ (𝑟 ∩ 𝑠)) |
48 | 47 | ex 413 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (((𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟) ∧ (𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠)) → ∃𝑡 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}𝑡 ⊆ (𝑟 ∩ 𝑠))) |
49 | 29, 48 | syl5bi 241 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ((𝑟 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∧ 𝑠 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}) → ∃𝑡 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}𝑡 ⊆ (𝑟 ∩ 𝑠))) |
50 | 49 | ralrimivv 3110 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ∀𝑟 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}∀𝑠 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}∃𝑡 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}𝑡 ⊆ (𝑟 ∩ 𝑠)) |
51 | 14, 24, 50 | 3jca 1127 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ≠ ∅ ∧ ∅ ∉ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∧ ∀𝑟 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}∀𝑠 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}∃𝑡 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}𝑡 ⊆ (𝑟 ∩ 𝑠))) |
52 | | isfbas2 22984 |
. . . 4
⊢ (𝑋 ∈ 𝐽 → ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∈ (fBas‘𝑋) ↔ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ⊆ 𝒫 𝑋 ∧ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ≠ ∅ ∧ ∅ ∉ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∧ ∀𝑟 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}∀𝑠 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}∃𝑡 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}𝑡 ⊆ (𝑟 ∩ 𝑠))))) |
53 | 8, 52 | syl 17 |
. . 3
⊢ (𝐽 ∈ Top → ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∈ (fBas‘𝑋) ↔ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ⊆ 𝒫 𝑋 ∧ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ≠ ∅ ∧ ∅ ∉ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∧ ∀𝑟 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}∀𝑠 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}∃𝑡 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}𝑡 ⊆ (𝑟 ∩ 𝑠))))) |
54 | 53 | 3ad2ant1 1132 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∈ (fBas‘𝑋) ↔ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ⊆ 𝒫 𝑋 ∧ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ≠ ∅ ∧ ∅ ∉ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∧ ∀𝑟 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}∀𝑠 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}∃𝑡 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}𝑡 ⊆ (𝑟 ∩ 𝑠))))) |
55 | 7, 51, 54 | mpbir2and 710 |
1
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∈ (fBas‘𝑋)) |