Proof of Theorem baspartn
Step | Hyp | Ref
| Expression |
1 | | id 19 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑃 → 𝑥 ∈ 𝑃) |
2 | | pwidg 3580 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑃 → 𝑥 ∈ 𝒫 𝑥) |
3 | 1, 2 | elind 3312 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑃 → 𝑥 ∈ (𝑃 ∩ 𝒫 𝑥)) |
4 | | elssuni 3824 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑃 ∩ 𝒫 𝑥) → 𝑥 ⊆ ∪ (𝑃 ∩ 𝒫 𝑥)) |
5 | 3, 4 | syl 14 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑃 → 𝑥 ⊆ ∪ (𝑃 ∩ 𝒫 𝑥)) |
6 | | inidm 3336 |
. . . . . . . . 9
⊢ (𝑥 ∩ 𝑥) = 𝑥 |
7 | | ineq2 3322 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ∩ 𝑥) = (𝑥 ∩ 𝑦)) |
8 | 6, 7 | eqtr3id 2217 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → 𝑥 = (𝑥 ∩ 𝑦)) |
9 | 8 | pweqd 3571 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 (𝑥 ∩ 𝑦)) |
10 | 9 | ineq2d 3328 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑃 ∩ 𝒫 𝑥) = (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
11 | 10 | unieqd 3807 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ∪ (𝑃 ∩ 𝒫 𝑥) = ∪
(𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
12 | 8, 11 | sseq12d 3178 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ ∪ (𝑃 ∩ 𝒫 𝑥) ↔ (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)))) |
13 | 5, 12 | syl5ibcom 154 |
. . . . . 6
⊢ (𝑥 ∈ 𝑃 → (𝑥 = 𝑦 → (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)))) |
14 | | 0ss 3453 |
. . . . . . . 8
⊢ ∅
⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)) |
15 | | sseq1 3170 |
. . . . . . . 8
⊢ ((𝑥 ∩ 𝑦) = ∅ → ((𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)) ↔ ∅ ⊆ ∪ (𝑃
∩ 𝒫 (𝑥 ∩
𝑦)))) |
16 | 14, 15 | mpbiri 167 |
. . . . . . 7
⊢ ((𝑥 ∩ 𝑦) = ∅ → (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
17 | 16 | a1i 9 |
. . . . . 6
⊢ (𝑥 ∈ 𝑃 → ((𝑥 ∩ 𝑦) = ∅ → (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)))) |
18 | 13, 17 | jaod 712 |
. . . . 5
⊢ (𝑥 ∈ 𝑃 → ((𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)))) |
19 | 18 | ralimdv 2538 |
. . . 4
⊢ (𝑥 ∈ 𝑃 → (∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅) → ∀𝑦 ∈ 𝑃 (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)))) |
20 | 19 | ralimia 2531 |
. . 3
⊢
(∀𝑥 ∈
𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
21 | 20 | adantl 275 |
. 2
⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦))) |
22 | | isbasisg 12836 |
. . 3
⊢ (𝑃 ∈ 𝑉 → (𝑃 ∈ TopBases ↔ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)))) |
23 | 22 | adantr 274 |
. 2
⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → (𝑃 ∈ TopBases ↔ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)))) |
24 | 21, 23 | mpbird 166 |
1
⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → 𝑃 ∈ TopBases) |