Step | Hyp | Ref
| Expression |
1 | | inass 3785 |
. . . . 5
⊢ ((𝐴 ∩ 𝐾) ∩ ∪ 𝐽) = (𝐴 ∩ (𝐾 ∩ ∪ 𝐽)) |
2 | | in32 3787 |
. . . . 5
⊢ ((𝐴 ∩ 𝐾) ∩ ∪ 𝐽) = ((𝐴 ∩ ∪ 𝐽) ∩ 𝐾) |
3 | 1, 2 | eqtr3i 2634 |
. . . 4
⊢ (𝐴 ∩ (𝐾 ∩ ∪ 𝐽)) = ((𝐴 ∩ ∪ 𝐽) ∩ 𝐾) |
4 | | df-kgen 21147 |
. . . . . . . . . . . 12
⊢
𝑘Gen = (𝑗
∈ Top ↦ {𝑥
∈ 𝒫 ∪ 𝑗 ∣ ∀𝑦 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑦) ∈ Comp → (𝑥 ∩ 𝑦) ∈ (𝑗 ↾t 𝑦))}) |
5 | 4 | dmmptss 5548 |
. . . . . . . . . . 11
⊢ dom
𝑘Gen ⊆ Top |
6 | | elfvdm 6130 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(𝑘Gen‘𝐽)
→ 𝐽 ∈ dom
𝑘Gen) |
7 | 5, 6 | sseldi 3566 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(𝑘Gen‘𝐽)
→ 𝐽 ∈
Top) |
8 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → 𝐽
∈ Top) |
9 | | eqid 2610 |
. . . . . . . . . 10
⊢ ∪ 𝐽 =
∪ 𝐽 |
10 | 9 | toptopon 20548 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
11 | 8, 10 | sylib 207 |
. . . . . . . 8
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → 𝐽
∈ (TopOn‘∪ 𝐽)) |
12 | | simpl 472 |
. . . . . . . 8
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → 𝐴
∈ (𝑘Gen‘𝐽)) |
13 | | elkgen 21149 |
. . . . . . . . 9
⊢ (𝐽 ∈ (TopOn‘∪ 𝐽)
→ (𝐴 ∈
(𝑘Gen‘𝐽)
↔ (𝐴 ⊆ ∪ 𝐽
∧ ∀𝑦 ∈
𝒫 ∪ 𝐽((𝐽 ↾t 𝑦) ∈ Comp → (𝐴 ∩ 𝑦) ∈ (𝐽 ↾t 𝑦))))) |
14 | 13 | biimpa 500 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝐴 ∈
(𝑘Gen‘𝐽))
→ (𝐴 ⊆ ∪ 𝐽
∧ ∀𝑦 ∈
𝒫 ∪ 𝐽((𝐽 ↾t 𝑦) ∈ Comp → (𝐴 ∩ 𝑦) ∈ (𝐽 ↾t 𝑦)))) |
15 | 11, 12, 14 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → (𝐴
⊆ ∪ 𝐽 ∧ ∀𝑦 ∈ 𝒫 ∪ 𝐽((𝐽 ↾t 𝑦) ∈ Comp → (𝐴 ∩ 𝑦) ∈ (𝐽 ↾t 𝑦)))) |
16 | 15 | simpld 474 |
. . . . . 6
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → 𝐴
⊆ ∪ 𝐽) |
17 | | df-ss 3554 |
. . . . . 6
⊢ (𝐴 ⊆ ∪ 𝐽
↔ (𝐴 ∩ ∪ 𝐽) =
𝐴) |
18 | 16, 17 | sylib 207 |
. . . . 5
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → (𝐴
∩ ∪ 𝐽) = 𝐴) |
19 | 18 | ineq1d 3775 |
. . . 4
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → ((𝐴
∩ ∪ 𝐽) ∩ 𝐾) = (𝐴 ∩ 𝐾)) |
20 | 3, 19 | syl5eq 2656 |
. . 3
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → (𝐴
∩ (𝐾 ∩ ∪ 𝐽))
= (𝐴 ∩ 𝐾)) |
21 | | inss2 3796 |
. . . . 5
⊢ (𝐾 ∩ ∪ 𝐽)
⊆ ∪ 𝐽 |
22 | | cmptop 21008 |
. . . . . . . 8
⊢ ((𝐽 ↾t 𝐾) ∈ Comp → (𝐽 ↾t 𝐾) ∈ Top) |
23 | 22 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ Top) |
24 | | restrcl 20771 |
. . . . . . . 8
⊢ ((𝐽 ↾t 𝐾) ∈ Top → (𝐽 ∈ V ∧ 𝐾 ∈ V)) |
25 | 24 | simprd 478 |
. . . . . . 7
⊢ ((𝐽 ↾t 𝐾) ∈ Top → 𝐾 ∈ V) |
26 | 23, 25 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → 𝐾
∈ V) |
27 | | inex1g 4729 |
. . . . . 6
⊢ (𝐾 ∈ V → (𝐾 ∩ ∪ 𝐽)
∈ V) |
28 | | elpwg 4116 |
. . . . . 6
⊢ ((𝐾 ∩ ∪ 𝐽)
∈ V → ((𝐾 ∩
∪ 𝐽) ∈ 𝒫 ∪ 𝐽
↔ (𝐾 ∩ ∪ 𝐽)
⊆ ∪ 𝐽)) |
29 | 26, 27, 28 | 3syl 18 |
. . . . 5
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → ((𝐾
∩ ∪ 𝐽) ∈ 𝒫 ∪ 𝐽
↔ (𝐾 ∩ ∪ 𝐽)
⊆ ∪ 𝐽)) |
30 | 21, 29 | mpbiri 247 |
. . . 4
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → (𝐾
∩ ∪ 𝐽) ∈ 𝒫 ∪ 𝐽) |
31 | 15 | simprd 478 |
. . . 4
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → ∀𝑦 ∈ 𝒫 ∪ 𝐽((𝐽 ↾t 𝑦) ∈ Comp → (𝐴 ∩ 𝑦) ∈ (𝐽 ↾t 𝑦))) |
32 | 9 | restin 20780 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ V) → (𝐽 ↾t 𝐾) = (𝐽 ↾t (𝐾 ∩ ∪ 𝐽))) |
33 | 8, 26, 32 | syl2anc 691 |
. . . . 5
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾) =
(𝐽 ↾t
(𝐾 ∩ ∪ 𝐽))) |
34 | | simpr 476 |
. . . . 5
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ Comp) |
35 | 33, 34 | eqeltrrd 2689 |
. . . 4
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → (𝐽
↾t (𝐾
∩ ∪ 𝐽)) ∈ Comp) |
36 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑦 = (𝐾 ∩ ∪ 𝐽) → (𝐽 ↾t 𝑦) = (𝐽 ↾t (𝐾 ∩ ∪ 𝐽))) |
37 | 36 | eleq1d 2672 |
. . . . . 6
⊢ (𝑦 = (𝐾 ∩ ∪ 𝐽) → ((𝐽 ↾t 𝑦) ∈ Comp ↔ (𝐽 ↾t (𝐾 ∩ ∪ 𝐽)) ∈
Comp)) |
38 | | ineq2 3770 |
. . . . . . 7
⊢ (𝑦 = (𝐾 ∩ ∪ 𝐽) → (𝐴 ∩ 𝑦) = (𝐴 ∩ (𝐾 ∩ ∪ 𝐽))) |
39 | 38, 36 | eleq12d 2682 |
. . . . . 6
⊢ (𝑦 = (𝐾 ∩ ∪ 𝐽) → ((𝐴 ∩ 𝑦) ∈ (𝐽 ↾t 𝑦) ↔ (𝐴 ∩ (𝐾 ∩ ∪ 𝐽)) ∈ (𝐽 ↾t (𝐾 ∩ ∪ 𝐽)))) |
40 | 37, 39 | imbi12d 333 |
. . . . 5
⊢ (𝑦 = (𝐾 ∩ ∪ 𝐽) → (((𝐽 ↾t 𝑦) ∈ Comp → (𝐴 ∩ 𝑦) ∈ (𝐽 ↾t 𝑦)) ↔ ((𝐽 ↾t (𝐾 ∩ ∪ 𝐽)) ∈ Comp → (𝐴 ∩ (𝐾 ∩ ∪ 𝐽)) ∈ (𝐽 ↾t (𝐾 ∩ ∪ 𝐽))))) |
41 | 40 | rspcv 3278 |
. . . 4
⊢ ((𝐾 ∩ ∪ 𝐽)
∈ 𝒫 ∪ 𝐽 → (∀𝑦 ∈ 𝒫 ∪ 𝐽((𝐽 ↾t 𝑦) ∈ Comp → (𝐴 ∩ 𝑦) ∈ (𝐽 ↾t 𝑦)) → ((𝐽 ↾t (𝐾 ∩ ∪ 𝐽)) ∈ Comp → (𝐴 ∩ (𝐾 ∩ ∪ 𝐽)) ∈ (𝐽 ↾t (𝐾 ∩ ∪ 𝐽))))) |
42 | 30, 31, 35, 41 | syl3c 64 |
. . 3
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → (𝐴
∩ (𝐾 ∩ ∪ 𝐽))
∈ (𝐽
↾t (𝐾
∩ ∪ 𝐽))) |
43 | 20, 42 | eqeltrrd 2689 |
. 2
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → (𝐴
∩ 𝐾) ∈ (𝐽 ↾t (𝐾 ∩ ∪ 𝐽))) |
44 | 43, 33 | eleqtrrd 2691 |
1
⊢ ((𝐴 ∈
(𝑘Gen‘𝐽)
∧ (𝐽
↾t 𝐾)
∈ Comp) → (𝐴
∩ 𝐾) ∈ (𝐽 ↾t 𝐾)) |