| Step | Hyp | Ref
| Expression |
| 1 | | elcls3.1 |
. . . 4
⊢ (𝜑 → 𝐽 = (topGen‘𝐵)) |
| 2 | | elcls3.3 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ TopBases) |
| 3 | | tgcl 22976 |
. . . . 5
⊢ (𝐵 ∈ TopBases →
(topGen‘𝐵) ∈
Top) |
| 4 | 2, 3 | syl 17 |
. . . 4
⊢ (𝜑 → (topGen‘𝐵) ∈ Top) |
| 5 | 1, 4 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Top) |
| 6 | | elcls3.4 |
. . . 4
⊢ (𝜑 → 𝑆 ⊆ 𝑋) |
| 7 | | elcls3.2 |
. . . 4
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
| 8 | 6, 7 | sseqtrd 4020 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽) |
| 9 | | elcls3.5 |
. . . 4
⊢ (𝜑 → 𝑃 ∈ 𝑋) |
| 10 | 9, 7 | eleqtrd 2843 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ∪ 𝐽) |
| 11 | | eqid 2737 |
. . . 4
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 12 | 11 | elcls 23081 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽
∧ 𝑃 ∈ ∪ 𝐽)
→ (𝑃 ∈
((cls‘𝐽)‘𝑆) ↔ ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))) |
| 13 | 5, 8, 10, 12 | syl3anc 1373 |
. 2
⊢ (𝜑 → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))) |
| 14 | | bastg 22973 |
. . . . . . . . 9
⊢ (𝐵 ∈ TopBases → 𝐵 ⊆ (topGen‘𝐵)) |
| 15 | 2, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ (topGen‘𝐵)) |
| 16 | 15, 1 | sseqtrrd 4021 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆ 𝐽) |
| 17 | 16 | sseld 3982 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐽)) |
| 18 | 17 | imim1d 82 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝐽 → (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅)) → (𝑦 ∈ 𝐵 → (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅)))) |
| 19 | 18 | ralimdv2 3163 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) → ∀𝑦 ∈ 𝐵 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))) |
| 20 | | eleq2w 2825 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (𝑃 ∈ 𝑦 ↔ 𝑃 ∈ 𝑥)) |
| 21 | | ineq1 4213 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (𝑦 ∩ 𝑆) = (𝑥 ∩ 𝑆)) |
| 22 | 21 | neeq1d 3000 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((𝑦 ∩ 𝑆) ≠ ∅ ↔ (𝑥 ∩ 𝑆) ≠ ∅)) |
| 23 | 20, 22 | imbi12d 344 |
. . . . 5
⊢ (𝑦 = 𝑥 → ((𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) ↔ (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))) |
| 24 | 23 | cbvralvw 3237 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) ↔ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) |
| 25 | 19, 24 | imbitrdi 251 |
. . 3
⊢ (𝜑 → (∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) → ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))) |
| 26 | | simprl 771 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦)) → 𝑦 ∈ 𝐽) |
| 27 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦)) → 𝐽 = (topGen‘𝐵)) |
| 28 | 26, 27 | eleqtrd 2843 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦)) → 𝑦 ∈ (topGen‘𝐵)) |
| 29 | | simprr 773 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦)) → 𝑃 ∈ 𝑦) |
| 30 | | tg2 22972 |
. . . . . . 7
⊢ ((𝑦 ∈ (topGen‘𝐵) ∧ 𝑃 ∈ 𝑦) → ∃𝑧 ∈ 𝐵 (𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)) |
| 31 | 28, 29, 30 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦)) → ∃𝑧 ∈ 𝐵 (𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)) |
| 32 | | eleq2w 2825 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑧)) |
| 33 | | ineq1 4213 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (𝑥 ∩ 𝑆) = (𝑧 ∩ 𝑆)) |
| 34 | 33 | neeq1d 3000 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → ((𝑥 ∩ 𝑆) ≠ ∅ ↔ (𝑧 ∩ 𝑆) ≠ ∅)) |
| 35 | 32, 34 | imbi12d 344 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → ((𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) ↔ (𝑃 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅))) |
| 36 | 35 | rspccva 3621 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) ∧ 𝑧 ∈ 𝐵) → (𝑃 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅)) |
| 37 | 36 | imp 406 |
. . . . . . . . . . 11
⊢
(((∀𝑥 ∈
𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ 𝑃 ∈ 𝑧) → (𝑧 ∩ 𝑆) ≠ ∅) |
| 38 | | ssdisj 4460 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ⊆ 𝑦 ∧ (𝑦 ∩ 𝑆) = ∅) → (𝑧 ∩ 𝑆) = ∅) |
| 39 | 38 | ex 412 |
. . . . . . . . . . . 12
⊢ (𝑧 ⊆ 𝑦 → ((𝑦 ∩ 𝑆) = ∅ → (𝑧 ∩ 𝑆) = ∅)) |
| 40 | 39 | necon3d 2961 |
. . . . . . . . . . 11
⊢ (𝑧 ⊆ 𝑦 → ((𝑧 ∩ 𝑆) ≠ ∅ → (𝑦 ∩ 𝑆) ≠ ∅)) |
| 41 | 37, 40 | syl5com 31 |
. . . . . . . . . 10
⊢
(((∀𝑥 ∈
𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ 𝑃 ∈ 𝑧) → (𝑧 ⊆ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅)) |
| 42 | 41 | exp31 419 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) → (𝑧 ∈ 𝐵 → (𝑃 ∈ 𝑧 → (𝑧 ⊆ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅)))) |
| 43 | 42 | imp4a 422 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) → (𝑧 ∈ 𝐵 → ((𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦) → (𝑦 ∩ 𝑆) ≠ ∅))) |
| 44 | 43 | rexlimdv 3153 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) → (∃𝑧 ∈ 𝐵 (𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦) → (𝑦 ∩ 𝑆) ≠ ∅)) |
| 45 | 44 | ad2antlr 727 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦)) → (∃𝑧 ∈ 𝐵 (𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦) → (𝑦 ∩ 𝑆) ≠ ∅)) |
| 46 | 31, 45 | mpd 15 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦)) → (𝑦 ∩ 𝑆) ≠ ∅) |
| 47 | 46 | exp43 436 |
. . . 4
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) → (𝑦 ∈ 𝐽 → (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅)))) |
| 48 | 47 | ralrimdv 3152 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) → ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))) |
| 49 | 25, 48 | impbid 212 |
. 2
⊢ (𝜑 → (∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) ↔ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))) |
| 50 | 13, 49 | bitrd 279 |
1
⊢ (𝜑 → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))) |