Proof of Theorem baspartn
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | id 22 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝑃 → 𝑥 ∈ 𝑃) | 
| 2 |  | pwidg 4619 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝑃 → 𝑥 ∈ 𝒫 𝑥) | 
| 3 | 1, 2 | elind 4199 | . . . . . . . 8
⊢ (𝑥 ∈ 𝑃 → 𝑥 ∈ (𝑃 ∩ 𝒫 𝑥)) | 
| 4 |  | elssuni 4936 | . . . . . . . 8
⊢ (𝑥 ∈ (𝑃 ∩ 𝒫 𝑥) → 𝑥 ⊆ ∪ (𝑃 ∩ 𝒫 𝑥)) | 
| 5 | 3, 4 | syl 17 | . . . . . . 7
⊢ (𝑥 ∈ 𝑃 → 𝑥 ⊆ ∪ (𝑃 ∩ 𝒫 𝑥)) | 
| 6 |  | inidm 4226 | . . . . . . . . 9
⊢ (𝑥 ∩ 𝑥) = 𝑥 | 
| 7 |  | ineq2 4213 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ∩ 𝑥) = (𝑥 ∩ 𝑦)) | 
| 8 | 6, 7 | eqtr3id 2790 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → 𝑥 = (𝑥 ∩ 𝑦)) | 
| 9 | 8 | pweqd 4616 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 (𝑥 ∩ 𝑦)) | 
| 10 | 9 | ineq2d 4219 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑃 ∩ 𝒫 𝑥) = (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦))) | 
| 11 | 10 | unieqd 4919 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → ∪ (𝑃 ∩ 𝒫 𝑥) = ∪
(𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦))) | 
| 12 | 8, 11 | sseq12d 4016 | . . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ ∪ (𝑃 ∩ 𝒫 𝑥) ↔ (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)))) | 
| 13 | 5, 12 | syl5ibcom 245 | . . . . . 6
⊢ (𝑥 ∈ 𝑃 → (𝑥 = 𝑦 → (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)))) | 
| 14 |  | 0ss 4399 | . . . . . . . 8
⊢ ∅
⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)) | 
| 15 |  | sseq1 4008 | . . . . . . . 8
⊢ ((𝑥 ∩ 𝑦) = ∅ → ((𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)) ↔ ∅ ⊆ ∪ (𝑃
∩ 𝒫 (𝑥 ∩
𝑦)))) | 
| 16 | 14, 15 | mpbiri 258 | . . . . . . 7
⊢ ((𝑥 ∩ 𝑦) = ∅ → (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦))) | 
| 17 | 16 | a1i 11 | . . . . . 6
⊢ (𝑥 ∈ 𝑃 → ((𝑥 ∩ 𝑦) = ∅ → (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)))) | 
| 18 | 13, 17 | jaod 859 | . . . . 5
⊢ (𝑥 ∈ 𝑃 → ((𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)))) | 
| 19 | 18 | ralimdv 3168 | . . . 4
⊢ (𝑥 ∈ 𝑃 → (∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅) → ∀𝑦 ∈ 𝑃 (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)))) | 
| 20 | 19 | ralimia 3079 | . . 3
⊢
(∀𝑥 ∈
𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦))) | 
| 21 | 20 | adantl 481 | . 2
⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦))) | 
| 22 |  | isbasisg 22955 | . . 3
⊢ (𝑃 ∈ 𝑉 → (𝑃 ∈ TopBases ↔ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)))) | 
| 23 | 22 | adantr 480 | . 2
⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → (𝑃 ∈ TopBases ↔ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 ∩ 𝑦) ⊆ ∪ (𝑃 ∩ 𝒫 (𝑥 ∩ 𝑦)))) | 
| 24 | 21, 23 | mpbird 257 | 1
⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → 𝑃 ∈ TopBases) |