Proof of Theorem kgencmp2
Step | Hyp | Ref
| Expression |
1 | | kgencmp 21158 |
. . 3
⊢ ((𝐽 ∈ Top ∧ (𝐽 ↾t 𝐾) ∈ Comp) → (𝐽 ↾t 𝐾) = ((𝑘Gen‘𝐽) ↾t 𝐾)) |
2 | | simpr 476 |
. . 3
⊢ ((𝐽 ∈ Top ∧ (𝐽 ↾t 𝐾) ∈ Comp) → (𝐽 ↾t 𝐾) ∈ Comp) |
3 | 1, 2 | eqeltrrd 2689 |
. 2
⊢ ((𝐽 ∈ Top ∧ (𝐽 ↾t 𝐾) ∈ Comp) →
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) |
4 | | cmptop 21008 |
. . . . . . 7
⊢
(((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp →
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Top) |
5 | | restrcl 20771 |
. . . . . . . 8
⊢
(((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Top →
((𝑘Gen‘𝐽)
∈ V ∧ 𝐾 ∈
V)) |
6 | 5 | simprd 478 |
. . . . . . 7
⊢
(((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Top → 𝐾 ∈ V) |
7 | 4, 6 | syl 17 |
. . . . . 6
⊢
(((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp → 𝐾 ∈ V) |
8 | | resttop 20774 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ V) → (𝐽 ↾t 𝐾) ∈ Top) |
9 | 7, 8 | sylan2 490 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ Top) |
10 | | eqid 2610 |
. . . . . 6
⊢ ∪ (𝐽
↾t 𝐾) =
∪ (𝐽 ↾t 𝐾) |
11 | 10 | toptopon 20548 |
. . . . 5
⊢ ((𝐽 ↾t 𝐾) ∈ Top ↔ (𝐽 ↾t 𝐾) ∈ (TopOn‘∪ (𝐽
↾t 𝐾))) |
12 | 9, 11 | sylib 207 |
. . . 4
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ (TopOn‘∪ (𝐽 ↾t 𝐾))) |
13 | | eqid 2610 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
14 | 13 | kgenuni 21152 |
. . . . . . . 8
⊢ (𝐽 ∈ Top → ∪ 𝐽 =
∪ (𝑘Gen‘𝐽)) |
15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → ∪ 𝐽 = ∪
(𝑘Gen‘𝐽)) |
16 | 15 | ineq2d 3776 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐾
∩ ∪ 𝐽) = (𝐾 ∩ ∪
(𝑘Gen‘𝐽))) |
17 | 13 | restuni2 20781 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ V) → (𝐾 ∩ ∪ 𝐽) =
∪ (𝐽 ↾t 𝐾)) |
18 | 7, 17 | sylan2 490 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐾
∩ ∪ 𝐽) = ∪ (𝐽 ↾t 𝐾)) |
19 | | kgenftop 21153 |
. . . . . . 7
⊢ (𝐽 ∈ Top →
(𝑘Gen‘𝐽)
∈ Top) |
20 | | eqid 2610 |
. . . . . . . 8
⊢ ∪ (𝑘Gen‘𝐽) = ∪
(𝑘Gen‘𝐽) |
21 | 20 | restuni2 20781 |
. . . . . . 7
⊢
(((𝑘Gen‘𝐽) ∈ Top ∧ 𝐾 ∈ V) → (𝐾 ∩ ∪
(𝑘Gen‘𝐽)) =
∪ ((𝑘Gen‘𝐽) ↾t 𝐾)) |
22 | 19, 7, 21 | syl2an 493 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐾
∩ ∪ (𝑘Gen‘𝐽)) = ∪
((𝑘Gen‘𝐽)
↾t 𝐾)) |
23 | 16, 18, 22 | 3eqtr3d 2652 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → ∪ (𝐽 ↾t 𝐾) = ∪
((𝑘Gen‘𝐽)
↾t 𝐾)) |
24 | 23 | fveq2d 6107 |
. . . 4
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (TopOn‘∪ (𝐽 ↾t 𝐾)) = (TopOn‘∪ ((𝑘Gen‘𝐽) ↾t 𝐾))) |
25 | 12, 24 | eleqtrd 2690 |
. . 3
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ (TopOn‘∪ ((𝑘Gen‘𝐽) ↾t 𝐾))) |
26 | | simpr 476 |
. . 3
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → ((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp) |
27 | 19 | adantr 480 |
. . . 4
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝑘Gen‘𝐽) ∈ Top) |
28 | | kgenss 21156 |
. . . . 5
⊢ (𝐽 ∈ Top → 𝐽 ⊆
(𝑘Gen‘𝐽)) |
29 | 28 | adantr 480 |
. . . 4
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → 𝐽
⊆ (𝑘Gen‘𝐽)) |
30 | | ssrest 20790 |
. . . 4
⊢
(((𝑘Gen‘𝐽) ∈ Top ∧ 𝐽 ⊆ (𝑘Gen‘𝐽)) → (𝐽 ↾t 𝐾) ⊆ ((𝑘Gen‘𝐽) ↾t 𝐾)) |
31 | 27, 29, 30 | syl2anc 691 |
. . 3
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
⊆ ((𝑘Gen‘𝐽) ↾t 𝐾)) |
32 | | eqid 2610 |
. . . 4
⊢ ∪ ((𝑘Gen‘𝐽) ↾t 𝐾) = ∪
((𝑘Gen‘𝐽)
↾t 𝐾) |
33 | 32 | sscmp 21018 |
. . 3
⊢ (((𝐽 ↾t 𝐾) ∈ (TopOn‘∪ ((𝑘Gen‘𝐽) ↾t 𝐾)) ∧ ((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp ∧ (𝐽 ↾t 𝐾) ⊆
((𝑘Gen‘𝐽)
↾t 𝐾))
→ (𝐽
↾t 𝐾)
∈ Comp) |
34 | 25, 26, 31, 33 | syl3anc 1318 |
. 2
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ Comp) |
35 | 3, 34 | impbida 873 |
1
⊢ (𝐽 ∈ Top → ((𝐽 ↾t 𝐾) ∈ Comp ↔
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp)) |