Proof of Theorem iincld
Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . . . 8
⊢ ∪ 𝐽 =
∪ 𝐽 |
2 | 1 | cldss 21926 |
. . . . . . 7
⊢ (𝐵 ∈ (Clsd‘𝐽) → 𝐵 ⊆ ∪ 𝐽) |
3 | | dfss4 4173 |
. . . . . . 7
⊢ (𝐵 ⊆ ∪ 𝐽
↔ (∪ 𝐽 ∖ (∪ 𝐽 ∖ 𝐵)) = 𝐵) |
4 | 2, 3 | sylib 221 |
. . . . . 6
⊢ (𝐵 ∈ (Clsd‘𝐽) → (∪ 𝐽
∖ (∪ 𝐽 ∖ 𝐵)) = 𝐵) |
5 | 4 | ralimi 3083 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ (Clsd‘𝐽) → ∀𝑥 ∈ 𝐴 (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝐵)) = 𝐵) |
6 | | iineq2 4924 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (∪ 𝐽
∖ (∪ 𝐽 ∖ 𝐵)) = 𝐵 → ∩
𝑥 ∈ 𝐴 (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝐵)) = ∩ 𝑥 ∈ 𝐴 𝐵) |
7 | 5, 6 | syl 17 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ (Clsd‘𝐽) → ∩
𝑥 ∈ 𝐴 (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝐵)) = ∩ 𝑥 ∈ 𝐴 𝐵) |
8 | 7 | adantl 485 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∩ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝐵)) = ∩ 𝑥 ∈ 𝐴 𝐵) |
9 | | iindif2 4985 |
. . . 4
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝐵)) = (∪ 𝐽
∖ ∪ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵))) |
10 | 9 | adantr 484 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∩ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝐵)) = (∪ 𝐽
∖ ∪ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵))) |
11 | 8, 10 | eqtr3d 2779 |
. 2
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∩ 𝑥 ∈ 𝐴 𝐵 = (∪ 𝐽 ∖ ∪ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵))) |
12 | | r19.2z 4406 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∃𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) |
13 | | cldrcl 21923 |
. . . . 5
⊢ (𝐵 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) |
14 | 13 | rexlimivw 3201 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 𝐵 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) |
15 | 12, 14 | syl 17 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → 𝐽 ∈ Top) |
16 | 1 | cldopn 21928 |
. . . . . 6
⊢ (𝐵 ∈ (Clsd‘𝐽) → (∪ 𝐽
∖ 𝐵) ∈ 𝐽) |
17 | 16 | ralimi 3083 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ (Clsd‘𝐽) → ∀𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵) ∈ 𝐽) |
18 | 17 | adantl 485 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∀𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵) ∈ 𝐽) |
19 | | iunopn 21795 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵) ∈ 𝐽) → ∪
𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵) ∈ 𝐽) |
20 | 15, 18, 19 | syl2anc 587 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∪ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵) ∈ 𝐽) |
21 | 1 | opncld 21930 |
. . 3
⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵) ∈ 𝐽) → (∪ 𝐽 ∖ ∪ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵)) ∈ (Clsd‘𝐽)) |
22 | 15, 20, 21 | syl2anc 587 |
. 2
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → (∪
𝐽 ∖ ∪ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵)) ∈ (Clsd‘𝐽)) |
23 | 11, 22 | eqeltrd 2838 |
1
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) |