Proof of Theorem topmeet
Step | Hyp | Ref
| Expression |
1 | | topmtcl 34479 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → (𝒫 𝑋 ∩ ∩ 𝑆) ∈ (TopOn‘𝑋)) |
2 | | inss2 4160 |
. . . . . . 7
⊢
(𝒫 𝑋 ∩
∩ 𝑆) ⊆ ∩ 𝑆 |
3 | | intss1 4891 |
. . . . . . 7
⊢ (𝑗 ∈ 𝑆 → ∩ 𝑆 ⊆ 𝑗) |
4 | 2, 3 | sstrid 3928 |
. . . . . 6
⊢ (𝑗 ∈ 𝑆 → (𝒫 𝑋 ∩ ∩ 𝑆) ⊆ 𝑗) |
5 | 4 | rgen 3073 |
. . . . 5
⊢
∀𝑗 ∈
𝑆 (𝒫 𝑋 ∩ ∩ 𝑆)
⊆ 𝑗 |
6 | | sseq1 3942 |
. . . . . . 7
⊢ (𝑘 = (𝒫 𝑋 ∩ ∩ 𝑆) → (𝑘 ⊆ 𝑗 ↔ (𝒫 𝑋 ∩ ∩ 𝑆) ⊆ 𝑗)) |
7 | 6 | ralbidv 3120 |
. . . . . 6
⊢ (𝑘 = (𝒫 𝑋 ∩ ∩ 𝑆) → (∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗 ↔ ∀𝑗 ∈ 𝑆 (𝒫 𝑋 ∩ ∩ 𝑆) ⊆ 𝑗)) |
8 | 7 | elrab 3617 |
. . . . 5
⊢
((𝒫 𝑋 ∩
∩ 𝑆) ∈ {𝑘 ∈ (TopOn‘𝑋) ∣ ∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗} ↔ ((𝒫 𝑋 ∩ ∩ 𝑆) ∈ (TopOn‘𝑋) ∧ ∀𝑗 ∈ 𝑆 (𝒫 𝑋 ∩ ∩ 𝑆) ⊆ 𝑗)) |
9 | 5, 8 | mpbiran2 706 |
. . . 4
⊢
((𝒫 𝑋 ∩
∩ 𝑆) ∈ {𝑘 ∈ (TopOn‘𝑋) ∣ ∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗} ↔ (𝒫 𝑋 ∩ ∩ 𝑆) ∈ (TopOn‘𝑋)) |
10 | 1, 9 | sylibr 233 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → (𝒫 𝑋 ∩ ∩ 𝑆) ∈ {𝑘 ∈ (TopOn‘𝑋) ∣ ∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗}) |
11 | | elssuni 4868 |
. . 3
⊢
((𝒫 𝑋 ∩
∩ 𝑆) ∈ {𝑘 ∈ (TopOn‘𝑋) ∣ ∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗} → (𝒫 𝑋 ∩ ∩ 𝑆) ⊆ ∪ {𝑘
∈ (TopOn‘𝑋)
∣ ∀𝑗 ∈
𝑆 𝑘 ⊆ 𝑗}) |
12 | 10, 11 | syl 17 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → (𝒫 𝑋 ∩ ∩ 𝑆) ⊆ ∪ {𝑘
∈ (TopOn‘𝑋)
∣ ∀𝑗 ∈
𝑆 𝑘 ⊆ 𝑗}) |
13 | | toponuni 21971 |
. . . . . . . . 9
⊢ (𝑘 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝑘) |
14 | | eqimss2 3974 |
. . . . . . . . 9
⊢ (𝑋 = ∪
𝑘 → ∪ 𝑘
⊆ 𝑋) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈ (TopOn‘𝑋) → ∪ 𝑘
⊆ 𝑋) |
16 | | sspwuni 5025 |
. . . . . . . 8
⊢ (𝑘 ⊆ 𝒫 𝑋 ↔ ∪ 𝑘
⊆ 𝑋) |
17 | 15, 16 | sylibr 233 |
. . . . . . 7
⊢ (𝑘 ∈ (TopOn‘𝑋) → 𝑘 ⊆ 𝒫 𝑋) |
18 | 17 | 3ad2ant2 1132 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) ∧ 𝑘 ∈ (TopOn‘𝑋) ∧ ∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗) → 𝑘 ⊆ 𝒫 𝑋) |
19 | | simp3 1136 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) ∧ 𝑘 ∈ (TopOn‘𝑋) ∧ ∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗) → ∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗) |
20 | | ssint 4892 |
. . . . . . 7
⊢ (𝑘 ⊆ ∩ 𝑆
↔ ∀𝑗 ∈
𝑆 𝑘 ⊆ 𝑗) |
21 | 19, 20 | sylibr 233 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) ∧ 𝑘 ∈ (TopOn‘𝑋) ∧ ∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗) → 𝑘 ⊆ ∩ 𝑆) |
22 | 18, 21 | ssind 4163 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) ∧ 𝑘 ∈ (TopOn‘𝑋) ∧ ∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗) → 𝑘 ⊆ (𝒫 𝑋 ∩ ∩ 𝑆)) |
23 | | velpw 4535 |
. . . . 5
⊢ (𝑘 ∈ 𝒫 (𝒫
𝑋 ∩ ∩ 𝑆)
↔ 𝑘 ⊆ (𝒫
𝑋 ∩ ∩ 𝑆)) |
24 | 22, 23 | sylibr 233 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) ∧ 𝑘 ∈ (TopOn‘𝑋) ∧ ∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗) → 𝑘 ∈ 𝒫 (𝒫 𝑋 ∩ ∩ 𝑆)) |
25 | 24 | rabssdv 4004 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → {𝑘 ∈ (TopOn‘𝑋) ∣ ∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗} ⊆ 𝒫 (𝒫 𝑋 ∩ ∩ 𝑆)) |
26 | | sspwuni 5025 |
. . 3
⊢ ({𝑘 ∈ (TopOn‘𝑋) ∣ ∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗} ⊆ 𝒫 (𝒫 𝑋 ∩ ∩ 𝑆)
↔ ∪ {𝑘 ∈ (TopOn‘𝑋) ∣ ∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗} ⊆ (𝒫 𝑋 ∩ ∩ 𝑆)) |
27 | 25, 26 | sylib 217 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → ∪
{𝑘 ∈
(TopOn‘𝑋) ∣
∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗} ⊆ (𝒫 𝑋 ∩ ∩ 𝑆)) |
28 | 12, 27 | eqssd 3934 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → (𝒫 𝑋 ∩ ∩ 𝑆) = ∪
{𝑘 ∈
(TopOn‘𝑋) ∣
∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗}) |