Proof of Theorem kgencmp2
Step | Hyp | Ref
| Expression |
1 | | kgencmp 22396 |
. . 3
⊢ ((𝐽 ∈ Top ∧ (𝐽 ↾t 𝐾) ∈ Comp) → (𝐽 ↾t 𝐾) = ((𝑘Gen‘𝐽) ↾t 𝐾)) |
2 | | simpr 488 |
. . 3
⊢ ((𝐽 ∈ Top ∧ (𝐽 ↾t 𝐾) ∈ Comp) → (𝐽 ↾t 𝐾) ∈ Comp) |
3 | 1, 2 | eqeltrrd 2832 |
. 2
⊢ ((𝐽 ∈ Top ∧ (𝐽 ↾t 𝐾) ∈ Comp) →
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) |
4 | | cmptop 22246 |
. . . . . . 7
⊢
(((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp →
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Top) |
5 | | restrcl 22008 |
. . . . . . . 8
⊢
(((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Top →
((𝑘Gen‘𝐽)
∈ V ∧ 𝐾 ∈
V)) |
6 | 5 | simprd 499 |
. . . . . . 7
⊢
(((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Top → 𝐾 ∈ V) |
7 | 4, 6 | syl 17 |
. . . . . 6
⊢
(((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp → 𝐾 ∈ V) |
8 | | resttop 22011 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ V) → (𝐽 ↾t 𝐾) ∈ Top) |
9 | 7, 8 | sylan2 596 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ Top) |
10 | | toptopon2 21769 |
. . . . 5
⊢ ((𝐽 ↾t 𝐾) ∈ Top ↔ (𝐽 ↾t 𝐾) ∈ (TopOn‘∪ (𝐽
↾t 𝐾))) |
11 | 9, 10 | sylib 221 |
. . . 4
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ (TopOn‘∪ (𝐽 ↾t 𝐾))) |
12 | | eqid 2736 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
13 | 12 | kgenuni 22390 |
. . . . . . . 8
⊢ (𝐽 ∈ Top → ∪ 𝐽 =
∪ (𝑘Gen‘𝐽)) |
14 | 13 | adantr 484 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → ∪ 𝐽 = ∪
(𝑘Gen‘𝐽)) |
15 | 14 | ineq2d 4113 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐾
∩ ∪ 𝐽) = (𝐾 ∩ ∪
(𝑘Gen‘𝐽))) |
16 | 12 | restuni2 22018 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ V) → (𝐾 ∩ ∪ 𝐽) =
∪ (𝐽 ↾t 𝐾)) |
17 | 7, 16 | sylan2 596 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐾
∩ ∪ 𝐽) = ∪ (𝐽 ↾t 𝐾)) |
18 | | kgenftop 22391 |
. . . . . . 7
⊢ (𝐽 ∈ Top →
(𝑘Gen‘𝐽)
∈ Top) |
19 | | eqid 2736 |
. . . . . . . 8
⊢ ∪ (𝑘Gen‘𝐽) = ∪
(𝑘Gen‘𝐽) |
20 | 19 | restuni2 22018 |
. . . . . . 7
⊢
(((𝑘Gen‘𝐽) ∈ Top ∧ 𝐾 ∈ V) → (𝐾 ∩ ∪
(𝑘Gen‘𝐽)) =
∪ ((𝑘Gen‘𝐽) ↾t 𝐾)) |
21 | 18, 7, 20 | syl2an 599 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐾
∩ ∪ (𝑘Gen‘𝐽)) = ∪
((𝑘Gen‘𝐽)
↾t 𝐾)) |
22 | 15, 17, 21 | 3eqtr3d 2779 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → ∪ (𝐽 ↾t 𝐾) = ∪
((𝑘Gen‘𝐽)
↾t 𝐾)) |
23 | 22 | fveq2d 6699 |
. . . 4
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (TopOn‘∪ (𝐽 ↾t 𝐾)) = (TopOn‘∪ ((𝑘Gen‘𝐽) ↾t 𝐾))) |
24 | 11, 23 | eleqtrd 2833 |
. . 3
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ (TopOn‘∪ ((𝑘Gen‘𝐽) ↾t 𝐾))) |
25 | | simpr 488 |
. . 3
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → ((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp) |
26 | | kgenss 22394 |
. . . . 5
⊢ (𝐽 ∈ Top → 𝐽 ⊆
(𝑘Gen‘𝐽)) |
27 | 26 | adantr 484 |
. . . 4
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → 𝐽
⊆ (𝑘Gen‘𝐽)) |
28 | | ssrest 22027 |
. . . 4
⊢
(((𝑘Gen‘𝐽) ∈ Top ∧ 𝐽 ⊆ (𝑘Gen‘𝐽)) → (𝐽 ↾t 𝐾) ⊆ ((𝑘Gen‘𝐽) ↾t 𝐾)) |
29 | 18, 27, 28 | syl2an2r 685 |
. . 3
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
⊆ ((𝑘Gen‘𝐽) ↾t 𝐾)) |
30 | | eqid 2736 |
. . . 4
⊢ ∪ ((𝑘Gen‘𝐽) ↾t 𝐾) = ∪
((𝑘Gen‘𝐽)
↾t 𝐾) |
31 | 30 | sscmp 22256 |
. . 3
⊢ (((𝐽 ↾t 𝐾) ∈ (TopOn‘∪ ((𝑘Gen‘𝐽) ↾t 𝐾)) ∧ ((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp ∧ (𝐽 ↾t 𝐾) ⊆
((𝑘Gen‘𝐽)
↾t 𝐾))
→ (𝐽
↾t 𝐾)
∈ Comp) |
32 | 24, 25, 29, 31 | syl3anc 1373 |
. 2
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ Comp) |
33 | 3, 32 | impbida 801 |
1
⊢ (𝐽 ∈ Top → ((𝐽 ↾t 𝐾) ∈ Comp ↔
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp)) |