Proof of Theorem kgencmp2
Step | Hyp | Ref
| Expression |
1 | | kgencmp 21569 |
. . 3
⊢ ((𝐽 ∈ Top ∧ (𝐽 ↾t 𝐾) ∈ Comp) → (𝐽 ↾t 𝐾) = ((𝑘Gen‘𝐽) ↾t 𝐾)) |
2 | | simpr 471 |
. . 3
⊢ ((𝐽 ∈ Top ∧ (𝐽 ↾t 𝐾) ∈ Comp) → (𝐽 ↾t 𝐾) ∈ Comp) |
3 | 1, 2 | eqeltrrd 2851 |
. 2
⊢ ((𝐽 ∈ Top ∧ (𝐽 ↾t 𝐾) ∈ Comp) →
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) |
4 | | cmptop 21419 |
. . . . . . 7
⊢
(((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp →
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Top) |
5 | | restrcl 21182 |
. . . . . . . 8
⊢
(((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Top →
((𝑘Gen‘𝐽)
∈ V ∧ 𝐾 ∈
V)) |
6 | 5 | simprd 483 |
. . . . . . 7
⊢
(((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Top → 𝐾 ∈ V) |
7 | 4, 6 | syl 17 |
. . . . . 6
⊢
(((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp → 𝐾 ∈ V) |
8 | | resttop 21185 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ V) → (𝐽 ↾t 𝐾) ∈ Top) |
9 | 7, 8 | sylan2 580 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ Top) |
10 | | eqid 2771 |
. . . . . 6
⊢ ∪ (𝐽
↾t 𝐾) =
∪ (𝐽 ↾t 𝐾) |
11 | 10 | toptopon 20942 |
. . . . 5
⊢ ((𝐽 ↾t 𝐾) ∈ Top ↔ (𝐽 ↾t 𝐾) ∈ (TopOn‘∪ (𝐽
↾t 𝐾))) |
12 | 9, 11 | sylib 208 |
. . . 4
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ (TopOn‘∪ (𝐽 ↾t 𝐾))) |
13 | | eqid 2771 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
14 | 13 | kgenuni 21563 |
. . . . . . . 8
⊢ (𝐽 ∈ Top → ∪ 𝐽 =
∪ (𝑘Gen‘𝐽)) |
15 | 14 | adantr 466 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → ∪ 𝐽 = ∪
(𝑘Gen‘𝐽)) |
16 | 15 | ineq2d 3965 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐾
∩ ∪ 𝐽) = (𝐾 ∩ ∪
(𝑘Gen‘𝐽))) |
17 | 13 | restuni2 21192 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ V) → (𝐾 ∩ ∪ 𝐽) =
∪ (𝐽 ↾t 𝐾)) |
18 | 7, 17 | sylan2 580 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐾
∩ ∪ 𝐽) = ∪ (𝐽 ↾t 𝐾)) |
19 | | kgenftop 21564 |
. . . . . . 7
⊢ (𝐽 ∈ Top →
(𝑘Gen‘𝐽)
∈ Top) |
20 | | eqid 2771 |
. . . . . . . 8
⊢ ∪ (𝑘Gen‘𝐽) = ∪
(𝑘Gen‘𝐽) |
21 | 20 | restuni2 21192 |
. . . . . . 7
⊢
(((𝑘Gen‘𝐽) ∈ Top ∧ 𝐾 ∈ V) → (𝐾 ∩ ∪
(𝑘Gen‘𝐽)) =
∪ ((𝑘Gen‘𝐽) ↾t 𝐾)) |
22 | 19, 7, 21 | syl2an 583 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐾
∩ ∪ (𝑘Gen‘𝐽)) = ∪
((𝑘Gen‘𝐽)
↾t 𝐾)) |
23 | 16, 18, 22 | 3eqtr3d 2813 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → ∪ (𝐽 ↾t 𝐾) = ∪
((𝑘Gen‘𝐽)
↾t 𝐾)) |
24 | 23 | fveq2d 6336 |
. . . 4
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (TopOn‘∪ (𝐽 ↾t 𝐾)) = (TopOn‘∪ ((𝑘Gen‘𝐽) ↾t 𝐾))) |
25 | 12, 24 | eleqtrd 2852 |
. . 3
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ (TopOn‘∪ ((𝑘Gen‘𝐽) ↾t 𝐾))) |
26 | | simpr 471 |
. . 3
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → ((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp) |
27 | 19 | adantr 466 |
. . . 4
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝑘Gen‘𝐽) ∈ Top) |
28 | | kgenss 21567 |
. . . . 5
⊢ (𝐽 ∈ Top → 𝐽 ⊆
(𝑘Gen‘𝐽)) |
29 | 28 | adantr 466 |
. . . 4
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → 𝐽
⊆ (𝑘Gen‘𝐽)) |
30 | | ssrest 21201 |
. . . 4
⊢
(((𝑘Gen‘𝐽) ∈ Top ∧ 𝐽 ⊆ (𝑘Gen‘𝐽)) → (𝐽 ↾t 𝐾) ⊆ ((𝑘Gen‘𝐽) ↾t 𝐾)) |
31 | 27, 29, 30 | syl2anc 573 |
. . 3
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
⊆ ((𝑘Gen‘𝐽) ↾t 𝐾)) |
32 | | eqid 2771 |
. . . 4
⊢ ∪ ((𝑘Gen‘𝐽) ↾t 𝐾) = ∪
((𝑘Gen‘𝐽)
↾t 𝐾) |
33 | 32 | sscmp 21429 |
. . 3
⊢ (((𝐽 ↾t 𝐾) ∈ (TopOn‘∪ ((𝑘Gen‘𝐽) ↾t 𝐾)) ∧ ((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp ∧ (𝐽 ↾t 𝐾) ⊆
((𝑘Gen‘𝐽)
↾t 𝐾))
→ (𝐽
↾t 𝐾)
∈ Comp) |
34 | 25, 26, 31, 33 | syl3anc 1476 |
. 2
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ Comp) |
35 | 3, 34 | impbida 802 |
1
⊢ (𝐽 ∈ Top → ((𝐽 ↾t 𝐾) ∈ Comp ↔
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp)) |