Proof of Theorem iincld
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . . . . . 8
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 2 | 1 | cldss 23038 | . . . . . . 7
⊢ (𝐵 ∈ (Clsd‘𝐽) → 𝐵 ⊆ ∪ 𝐽) | 
| 3 |  | dfss4 4268 | . . . . . . 7
⊢ (𝐵 ⊆ ∪ 𝐽
↔ (∪ 𝐽 ∖ (∪ 𝐽 ∖ 𝐵)) = 𝐵) | 
| 4 | 2, 3 | sylib 218 | . . . . . 6
⊢ (𝐵 ∈ (Clsd‘𝐽) → (∪ 𝐽
∖ (∪ 𝐽 ∖ 𝐵)) = 𝐵) | 
| 5 | 4 | ralimi 3082 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ (Clsd‘𝐽) → ∀𝑥 ∈ 𝐴 (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝐵)) = 𝐵) | 
| 6 |  | iineq2 5011 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 (∪ 𝐽
∖ (∪ 𝐽 ∖ 𝐵)) = 𝐵 → ∩
𝑥 ∈ 𝐴 (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝐵)) = ∩ 𝑥 ∈ 𝐴 𝐵) | 
| 7 | 5, 6 | syl 17 | . . . 4
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ (Clsd‘𝐽) → ∩
𝑥 ∈ 𝐴 (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝐵)) = ∩ 𝑥 ∈ 𝐴 𝐵) | 
| 8 | 7 | adantl 481 | . . 3
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∩ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝐵)) = ∩ 𝑥 ∈ 𝐴 𝐵) | 
| 9 |  | iindif2 5076 | . . . 4
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝐵)) = (∪ 𝐽
∖ ∪ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵))) | 
| 10 | 9 | adantr 480 | . . 3
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∩ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ (∪ 𝐽
∖ 𝐵)) = (∪ 𝐽
∖ ∪ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵))) | 
| 11 | 8, 10 | eqtr3d 2778 | . 2
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∩ 𝑥 ∈ 𝐴 𝐵 = (∪ 𝐽 ∖ ∪ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵))) | 
| 12 |  | r19.2z 4494 | . . . 4
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∃𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) | 
| 13 |  | cldrcl 23035 | . . . . 5
⊢ (𝐵 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) | 
| 14 | 13 | rexlimivw 3150 | . . . 4
⊢
(∃𝑥 ∈
𝐴 𝐵 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) | 
| 15 | 12, 14 | syl 17 | . . 3
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → 𝐽 ∈ Top) | 
| 16 | 1 | cldopn 23040 | . . . . . 6
⊢ (𝐵 ∈ (Clsd‘𝐽) → (∪ 𝐽
∖ 𝐵) ∈ 𝐽) | 
| 17 | 16 | ralimi 3082 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ (Clsd‘𝐽) → ∀𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵) ∈ 𝐽) | 
| 18 | 17 | adantl 481 | . . . 4
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∀𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵) ∈ 𝐽) | 
| 19 |  | iunopn 22905 | . . . 4
⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵) ∈ 𝐽) → ∪
𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵) ∈ 𝐽) | 
| 20 | 15, 18, 19 | syl2anc 584 | . . 3
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∪ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵) ∈ 𝐽) | 
| 21 | 1 | opncld 23042 | . . 3
⊢ ((𝐽 ∈ Top ∧ ∪ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵) ∈ 𝐽) → (∪ 𝐽 ∖ ∪ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵)) ∈ (Clsd‘𝐽)) | 
| 22 | 15, 20, 21 | syl2anc 584 | . 2
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → (∪
𝐽 ∖ ∪ 𝑥 ∈ 𝐴 (∪ 𝐽 ∖ 𝐵)) ∈ (Clsd‘𝐽)) | 
| 23 | 11, 22 | eqeltrd 2840 | 1
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) |