Step | Hyp | Ref
| Expression |
1 | | elcls3.1 |
. . . 4
⊢ (𝜑 → 𝐽 = (topGen‘𝐵)) |
2 | | elcls3.3 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ TopBases) |
3 | | tgcl 20584 |
. . . . 5
⊢ (𝐵 ∈ TopBases →
(topGen‘𝐵) ∈
Top) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (𝜑 → (topGen‘𝐵) ∈ Top) |
5 | 1, 4 | eqeltrd 2688 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Top) |
6 | | elcls3.4 |
. . . 4
⊢ (𝜑 → 𝑆 ⊆ 𝑋) |
7 | | elcls3.2 |
. . . 4
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
8 | 6, 7 | sseqtrd 3604 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽) |
9 | | elcls3.5 |
. . . 4
⊢ (𝜑 → 𝑃 ∈ 𝑋) |
10 | 9, 7 | eleqtrd 2690 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ∪ 𝐽) |
11 | | eqid 2610 |
. . . 4
⊢ ∪ 𝐽 =
∪ 𝐽 |
12 | 11 | elcls 20687 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽
∧ 𝑃 ∈ ∪ 𝐽)
→ (𝑃 ∈
((cls‘𝐽)‘𝑆) ↔ ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))) |
13 | 5, 8, 10, 12 | syl3anc 1318 |
. 2
⊢ (𝜑 → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))) |
14 | | bastg 20581 |
. . . . . . . . 9
⊢ (𝐵 ∈ TopBases → 𝐵 ⊆ (topGen‘𝐵)) |
15 | 2, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ (topGen‘𝐵)) |
16 | 15, 1 | sseqtr4d 3605 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆ 𝐽) |
17 | 16 | sseld 3567 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐽)) |
18 | 17 | imim1d 80 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝐽 → (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅)) → (𝑦 ∈ 𝐵 → (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅)))) |
19 | 18 | ralimdv2 2944 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) → ∀𝑦 ∈ 𝐵 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))) |
20 | | eleq2 2677 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (𝑃 ∈ 𝑦 ↔ 𝑃 ∈ 𝑥)) |
21 | | ineq1 3769 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (𝑦 ∩ 𝑆) = (𝑥 ∩ 𝑆)) |
22 | 21 | neeq1d 2841 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((𝑦 ∩ 𝑆) ≠ ∅ ↔ (𝑥 ∩ 𝑆) ≠ ∅)) |
23 | 20, 22 | imbi12d 333 |
. . . . 5
⊢ (𝑦 = 𝑥 → ((𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) ↔ (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))) |
24 | 23 | cbvralv 3147 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) ↔ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) |
25 | 19, 24 | syl6ib 240 |
. . 3
⊢ (𝜑 → (∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) → ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))) |
26 | | simprl 790 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦)) → 𝑦 ∈ 𝐽) |
27 | 1 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦)) → 𝐽 = (topGen‘𝐵)) |
28 | 26, 27 | eleqtrd 2690 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦)) → 𝑦 ∈ (topGen‘𝐵)) |
29 | | simprr 792 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦)) → 𝑃 ∈ 𝑦) |
30 | | tg2 20580 |
. . . . . . 7
⊢ ((𝑦 ∈ (topGen‘𝐵) ∧ 𝑃 ∈ 𝑦) → ∃𝑧 ∈ 𝐵 (𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)) |
31 | 28, 29, 30 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦)) → ∃𝑧 ∈ 𝐵 (𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)) |
32 | | eleq2 2677 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑧)) |
33 | | ineq1 3769 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (𝑥 ∩ 𝑆) = (𝑧 ∩ 𝑆)) |
34 | 33 | neeq1d 2841 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → ((𝑥 ∩ 𝑆) ≠ ∅ ↔ (𝑧 ∩ 𝑆) ≠ ∅)) |
35 | 32, 34 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → ((𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) ↔ (𝑃 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅))) |
36 | 35 | rspccva 3281 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) ∧ 𝑧 ∈ 𝐵) → (𝑃 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅)) |
37 | 36 | imp 444 |
. . . . . . . . . . 11
⊢
(((∀𝑥 ∈
𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ 𝑃 ∈ 𝑧) → (𝑧 ∩ 𝑆) ≠ ∅) |
38 | | ssdisj 3978 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ⊆ 𝑦 ∧ (𝑦 ∩ 𝑆) = ∅) → (𝑧 ∩ 𝑆) = ∅) |
39 | 38 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑧 ⊆ 𝑦 → ((𝑦 ∩ 𝑆) = ∅ → (𝑧 ∩ 𝑆) = ∅)) |
40 | 39 | necon3d 2803 |
. . . . . . . . . . 11
⊢ (𝑧 ⊆ 𝑦 → ((𝑧 ∩ 𝑆) ≠ ∅ → (𝑦 ∩ 𝑆) ≠ ∅)) |
41 | 37, 40 | syl5com 31 |
. . . . . . . . . 10
⊢
(((∀𝑥 ∈
𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ 𝑃 ∈ 𝑧) → (𝑧 ⊆ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅)) |
42 | 41 | exp31 628 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) → (𝑧 ∈ 𝐵 → (𝑃 ∈ 𝑧 → (𝑧 ⊆ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅)))) |
43 | 42 | imp4a 612 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) → (𝑧 ∈ 𝐵 → ((𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦) → (𝑦 ∩ 𝑆) ≠ ∅))) |
44 | 43 | rexlimdv 3012 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) → (∃𝑧 ∈ 𝐵 (𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦) → (𝑦 ∩ 𝑆) ≠ ∅)) |
45 | 44 | ad2antlr 759 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦)) → (∃𝑧 ∈ 𝐵 (𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦) → (𝑦 ∩ 𝑆) ≠ ∅)) |
46 | 31, 45 | mpd 15 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦)) → (𝑦 ∩ 𝑆) ≠ ∅) |
47 | 46 | exp43 638 |
. . . 4
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) → (𝑦 ∈ 𝐽 → (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅)))) |
48 | 47 | ralrimdv 2951 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅) → ∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅))) |
49 | 25, 48 | impbid 201 |
. 2
⊢ (𝜑 → (∀𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 → (𝑦 ∩ 𝑆) ≠ ∅) ↔ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))) |
50 | 13, 49 | bitrd 267 |
1
⊢ (𝜑 → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))) |