Step | Hyp | Ref
| Expression |
1 | | fclsbas.f |
. . . 4
⊢ 𝐹 = (𝑋filGen𝐵) |
2 | | fgcl 22775 |
. . . . 5
⊢ (𝐵 ∈ (fBas‘𝑋) → (𝑋filGen𝐵) ∈ (Fil‘𝑋)) |
3 | 2 | adantl 485 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → (𝑋filGen𝐵) ∈ (Fil‘𝑋)) |
4 | 1, 3 | eqeltrid 2842 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → 𝐹 ∈ (Fil‘𝑋)) |
5 | | fclsopn 22911 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∀𝑡 ∈ 𝐹 (𝑜 ∩ 𝑡) ≠ ∅)))) |
6 | 4, 5 | syldan 594 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∀𝑡 ∈ 𝐹 (𝑜 ∩ 𝑡) ≠ ∅)))) |
7 | | ssfg 22769 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (fBas‘𝑋) → 𝐵 ⊆ (𝑋filGen𝐵)) |
8 | 7 | ad3antlr 731 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ (𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜)) → 𝐵 ⊆ (𝑋filGen𝐵)) |
9 | 8, 1 | sseqtrrdi 3952 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ (𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜)) → 𝐵 ⊆ 𝐹) |
10 | | ssralv 3967 |
. . . . . . . . 9
⊢ (𝐵 ⊆ 𝐹 → (∀𝑡 ∈ 𝐹 (𝑜 ∩ 𝑡) ≠ ∅ → ∀𝑡 ∈ 𝐵 (𝑜 ∩ 𝑡) ≠ ∅)) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ (𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜)) → (∀𝑡 ∈ 𝐹 (𝑜 ∩ 𝑡) ≠ ∅ → ∀𝑡 ∈ 𝐵 (𝑜 ∩ 𝑡) ≠ ∅)) |
12 | | ineq2 4121 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑠 → (𝑜 ∩ 𝑡) = (𝑜 ∩ 𝑠)) |
13 | 12 | neeq1d 3000 |
. . . . . . . . 9
⊢ (𝑡 = 𝑠 → ((𝑜 ∩ 𝑡) ≠ ∅ ↔ (𝑜 ∩ 𝑠) ≠ ∅)) |
14 | 13 | cbvralvw 3358 |
. . . . . . . 8
⊢
(∀𝑡 ∈
𝐵 (𝑜 ∩ 𝑡) ≠ ∅ ↔ ∀𝑠 ∈ 𝐵 (𝑜 ∩ 𝑠) ≠ ∅) |
15 | 11, 14 | syl6ib 254 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ (𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜)) → (∀𝑡 ∈ 𝐹 (𝑜 ∩ 𝑡) ≠ ∅ → ∀𝑠 ∈ 𝐵 (𝑜 ∩ 𝑠) ≠ ∅)) |
16 | 1 | eleq2i 2829 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ 𝐹 ↔ 𝑡 ∈ (𝑋filGen𝐵)) |
17 | | elfg 22768 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (fBas‘𝑋) → (𝑡 ∈ (𝑋filGen𝐵) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡))) |
18 | 17 | ad3antlr 731 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ (𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜)) → (𝑡 ∈ (𝑋filGen𝐵) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡))) |
19 | 16, 18 | syl5bb 286 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ (𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜)) → (𝑡 ∈ 𝐹 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡))) |
20 | 19 | simplbda 503 |
. . . . . . . . 9
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ (𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜)) ∧ 𝑡 ∈ 𝐹) → ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡) |
21 | | r19.29r 3177 |
. . . . . . . . . . 11
⊢
((∃𝑠 ∈
𝐵 𝑠 ⊆ 𝑡 ∧ ∀𝑠 ∈ 𝐵 (𝑜 ∩ 𝑠) ≠ ∅) → ∃𝑠 ∈ 𝐵 (𝑠 ⊆ 𝑡 ∧ (𝑜 ∩ 𝑠) ≠ ∅)) |
22 | | sslin 4149 |
. . . . . . . . . . . . 13
⊢ (𝑠 ⊆ 𝑡 → (𝑜 ∩ 𝑠) ⊆ (𝑜 ∩ 𝑡)) |
23 | | ssn0 4315 |
. . . . . . . . . . . . 13
⊢ (((𝑜 ∩ 𝑠) ⊆ (𝑜 ∩ 𝑡) ∧ (𝑜 ∩ 𝑠) ≠ ∅) → (𝑜 ∩ 𝑡) ≠ ∅) |
24 | 22, 23 | sylan 583 |
. . . . . . . . . . . 12
⊢ ((𝑠 ⊆ 𝑡 ∧ (𝑜 ∩ 𝑠) ≠ ∅) → (𝑜 ∩ 𝑡) ≠ ∅) |
25 | 24 | rexlimivw 3201 |
. . . . . . . . . . 11
⊢
(∃𝑠 ∈
𝐵 (𝑠 ⊆ 𝑡 ∧ (𝑜 ∩ 𝑠) ≠ ∅) → (𝑜 ∩ 𝑡) ≠ ∅) |
26 | 21, 25 | syl 17 |
. . . . . . . . . 10
⊢
((∃𝑠 ∈
𝐵 𝑠 ⊆ 𝑡 ∧ ∀𝑠 ∈ 𝐵 (𝑜 ∩ 𝑠) ≠ ∅) → (𝑜 ∩ 𝑡) ≠ ∅) |
27 | 26 | ex 416 |
. . . . . . . . 9
⊢
(∃𝑠 ∈
𝐵 𝑠 ⊆ 𝑡 → (∀𝑠 ∈ 𝐵 (𝑜 ∩ 𝑠) ≠ ∅ → (𝑜 ∩ 𝑡) ≠ ∅)) |
28 | 20, 27 | syl 17 |
. . . . . . . 8
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ (𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜)) ∧ 𝑡 ∈ 𝐹) → (∀𝑠 ∈ 𝐵 (𝑜 ∩ 𝑠) ≠ ∅ → (𝑜 ∩ 𝑡) ≠ ∅)) |
29 | 28 | ralrimdva 3110 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ (𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜)) → (∀𝑠 ∈ 𝐵 (𝑜 ∩ 𝑠) ≠ ∅ → ∀𝑡 ∈ 𝐹 (𝑜 ∩ 𝑡) ≠ ∅)) |
30 | 15, 29 | impbid 215 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ (𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜)) → (∀𝑡 ∈ 𝐹 (𝑜 ∩ 𝑡) ≠ ∅ ↔ ∀𝑠 ∈ 𝐵 (𝑜 ∩ 𝑠) ≠ ∅)) |
31 | 30 | anassrs 471 |
. . . . 5
⊢
(((((𝐽 ∈
(TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑜 ∈ 𝐽) ∧ 𝐴 ∈ 𝑜) → (∀𝑡 ∈ 𝐹 (𝑜 ∩ 𝑡) ≠ ∅ ↔ ∀𝑠 ∈ 𝐵 (𝑜 ∩ 𝑠) ≠ ∅)) |
32 | 31 | pm5.74da 804 |
. . . 4
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) ∧ 𝑜 ∈ 𝐽) → ((𝐴 ∈ 𝑜 → ∀𝑡 ∈ 𝐹 (𝑜 ∩ 𝑡) ≠ ∅) ↔ (𝐴 ∈ 𝑜 → ∀𝑠 ∈ 𝐵 (𝑜 ∩ 𝑠) ≠ ∅))) |
33 | 32 | ralbidva 3117 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) ∧ 𝐴 ∈ 𝑋) → (∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∀𝑡 ∈ 𝐹 (𝑜 ∩ 𝑡) ≠ ∅) ↔ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∀𝑠 ∈ 𝐵 (𝑜 ∩ 𝑠) ≠ ∅))) |
34 | 33 | pm5.32da 582 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → ((𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∀𝑡 ∈ 𝐹 (𝑜 ∩ 𝑡) ≠ ∅)) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∀𝑠 ∈ 𝐵 (𝑜 ∩ 𝑠) ≠ ∅)))) |
35 | 6, 34 | bitrd 282 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∀𝑠 ∈ 𝐵 (𝑜 ∩ 𝑠) ≠ ∅)))) |