Step | Hyp | Ref
| Expression |
1 | | isclo.1 |
. . 3
⊢ 𝑋 = ∪
𝐽 |
2 | 1 | isclo 20939 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)))) |
3 | | eleq1 2718 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) |
4 | 3 | bibi2d 331 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑤 → ((𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))) |
5 | 4 | cbvralv 3201 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ↔ ∀𝑤 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) |
6 | 5 | anbi2i 730 |
. . . . . . . 8
⊢
((∀𝑧 ∈
𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) ↔ (∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ∧ ∀𝑤 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))) |
7 | | pm4.24 676 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ↔ (∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))) |
8 | | raaanv 4116 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑦 ∀𝑤 ∈ 𝑦 ((𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) ↔ (∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ∧ ∀𝑤 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))) |
9 | 6, 7, 8 | 3bitr4i 292 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ↔ ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 ((𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))) |
10 | | bibi1 340 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴) ↔ (𝑧 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))) |
11 | 10 | biimpa 500 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) → (𝑧 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) |
12 | 11 | biimpcd 239 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) → 𝑤 ∈ 𝐴)) |
13 | 12 | ralimdv 2992 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝐴 → (∀𝑤 ∈ 𝑦 ((𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) → ∀𝑤 ∈ 𝑦 𝑤 ∈ 𝐴)) |
14 | 13 | com12 32 |
. . . . . . . . 9
⊢
(∀𝑤 ∈
𝑦 ((𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) → (𝑧 ∈ 𝐴 → ∀𝑤 ∈ 𝑦 𝑤 ∈ 𝐴)) |
15 | | dfss3 3625 |
. . . . . . . . 9
⊢ (𝑦 ⊆ 𝐴 ↔ ∀𝑤 ∈ 𝑦 𝑤 ∈ 𝐴) |
16 | 14, 15 | syl6ibr 242 |
. . . . . . . 8
⊢
(∀𝑤 ∈
𝑦 ((𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) → (𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴)) |
17 | 16 | ralimi 2981 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝑦 ∀𝑤 ∈ 𝑦 ((𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) → ∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴)) |
18 | 9, 17 | sylbi 207 |
. . . . . 6
⊢
(∀𝑧 ∈
𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) → ∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴)) |
19 | | eleq1 2718 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)) |
20 | 19 | imbi1d 330 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → ((𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴) ↔ (𝑥 ∈ 𝐴 → 𝑦 ⊆ 𝐴))) |
21 | 20 | rspcv 3336 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑦 → (∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴) → (𝑥 ∈ 𝐴 → 𝑦 ⊆ 𝐴))) |
22 | | dfss3 3625 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ 𝐴 ↔ ∀𝑧 ∈ 𝑦 𝑧 ∈ 𝐴) |
23 | 22 | imbi2i 325 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 → 𝑦 ⊆ 𝐴) ↔ (𝑥 ∈ 𝐴 → ∀𝑧 ∈ 𝑦 𝑧 ∈ 𝐴)) |
24 | | r19.21v 2989 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
𝑦 (𝑥 ∈ 𝐴 → 𝑧 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 → ∀𝑧 ∈ 𝑦 𝑧 ∈ 𝐴)) |
25 | 23, 24 | bitr4i 267 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 → 𝑦 ⊆ 𝐴) ↔ ∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 → 𝑧 ∈ 𝐴)) |
26 | 21, 25 | syl6ib 241 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑦 → (∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴) → ∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 → 𝑧 ∈ 𝐴))) |
27 | | ssel 3630 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ∈ 𝐴)) |
28 | 27 | com12 32 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑦 → (𝑦 ⊆ 𝐴 → 𝑥 ∈ 𝐴)) |
29 | 28 | imim2d 57 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑦 → ((𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴) → (𝑧 ∈ 𝐴 → 𝑥 ∈ 𝐴))) |
30 | 29 | ralimdv 2992 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑦 → (∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴) → ∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑥 ∈ 𝐴))) |
31 | 26, 30 | jcad 554 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑦 → (∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴) → (∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 → 𝑧 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑥 ∈ 𝐴)))) |
32 | | ralbiim 3098 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ↔ (∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 → 𝑧 ∈ 𝐴) ∧ ∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑥 ∈ 𝐴))) |
33 | 31, 32 | syl6ibr 242 |
. . . . . 6
⊢ (𝑥 ∈ 𝑦 → (∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴) → ∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))) |
34 | 18, 33 | impbid2 216 |
. . . . 5
⊢ (𝑥 ∈ 𝑦 → (∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) ↔ ∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴))) |
35 | 34 | pm5.32i 670 |
. . . 4
⊢ ((𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴))) |
36 | 35 | rexbii 3070 |
. . 3
⊢
(∃𝑦 ∈
𝐽 (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) ↔ ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴))) |
37 | 36 | ralbii 3009 |
. 2
⊢
(∀𝑥 ∈
𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴))) |
38 | 2, 37 | syl6bb 276 |
1
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴)))) |