Proof of Theorem kgencmp2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | kgencmp 23554 | . . 3
⊢ ((𝐽 ∈ Top ∧ (𝐽 ↾t 𝐾) ∈ Comp) → (𝐽 ↾t 𝐾) = ((𝑘Gen‘𝐽) ↾t 𝐾)) | 
| 2 |  | simpr 484 | . . 3
⊢ ((𝐽 ∈ Top ∧ (𝐽 ↾t 𝐾) ∈ Comp) → (𝐽 ↾t 𝐾) ∈ Comp) | 
| 3 | 1, 2 | eqeltrrd 2841 | . 2
⊢ ((𝐽 ∈ Top ∧ (𝐽 ↾t 𝐾) ∈ Comp) →
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) | 
| 4 |  | cmptop 23404 | . . . . . . 7
⊢
(((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp →
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Top) | 
| 5 |  | restrcl 23166 | . . . . . . . 8
⊢
(((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Top →
((𝑘Gen‘𝐽)
∈ V ∧ 𝐾 ∈
V)) | 
| 6 | 5 | simprd 495 | . . . . . . 7
⊢
(((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Top → 𝐾 ∈ V) | 
| 7 | 4, 6 | syl 17 | . . . . . 6
⊢
(((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp → 𝐾 ∈ V) | 
| 8 |  | resttop 23169 | . . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ V) → (𝐽 ↾t 𝐾) ∈ Top) | 
| 9 | 7, 8 | sylan2 593 | . . . . 5
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ Top) | 
| 10 |  | toptopon2 22925 | . . . . 5
⊢ ((𝐽 ↾t 𝐾) ∈ Top ↔ (𝐽 ↾t 𝐾) ∈ (TopOn‘∪ (𝐽
↾t 𝐾))) | 
| 11 | 9, 10 | sylib 218 | . . . 4
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ (TopOn‘∪ (𝐽 ↾t 𝐾))) | 
| 12 |  | eqid 2736 | . . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 13 | 12 | kgenuni 23548 | . . . . . . . 8
⊢ (𝐽 ∈ Top → ∪ 𝐽 =
∪ (𝑘Gen‘𝐽)) | 
| 14 | 13 | adantr 480 | . . . . . . 7
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → ∪ 𝐽 = ∪
(𝑘Gen‘𝐽)) | 
| 15 | 14 | ineq2d 4219 | . . . . . 6
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐾
∩ ∪ 𝐽) = (𝐾 ∩ ∪
(𝑘Gen‘𝐽))) | 
| 16 | 12 | restuni2 23176 | . . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ V) → (𝐾 ∩ ∪ 𝐽) =
∪ (𝐽 ↾t 𝐾)) | 
| 17 | 7, 16 | sylan2 593 | . . . . . 6
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐾
∩ ∪ 𝐽) = ∪ (𝐽 ↾t 𝐾)) | 
| 18 |  | kgenftop 23549 | . . . . . . 7
⊢ (𝐽 ∈ Top →
(𝑘Gen‘𝐽)
∈ Top) | 
| 19 |  | eqid 2736 | . . . . . . . 8
⊢ ∪ (𝑘Gen‘𝐽) = ∪
(𝑘Gen‘𝐽) | 
| 20 | 19 | restuni2 23176 | . . . . . . 7
⊢
(((𝑘Gen‘𝐽) ∈ Top ∧ 𝐾 ∈ V) → (𝐾 ∩ ∪
(𝑘Gen‘𝐽)) =
∪ ((𝑘Gen‘𝐽) ↾t 𝐾)) | 
| 21 | 18, 7, 20 | syl2an 596 | . . . . . 6
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐾
∩ ∪ (𝑘Gen‘𝐽)) = ∪
((𝑘Gen‘𝐽)
↾t 𝐾)) | 
| 22 | 15, 17, 21 | 3eqtr3d 2784 | . . . . 5
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → ∪ (𝐽 ↾t 𝐾) = ∪
((𝑘Gen‘𝐽)
↾t 𝐾)) | 
| 23 | 22 | fveq2d 6909 | . . . 4
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (TopOn‘∪ (𝐽 ↾t 𝐾)) = (TopOn‘∪ ((𝑘Gen‘𝐽) ↾t 𝐾))) | 
| 24 | 11, 23 | eleqtrd 2842 | . . 3
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ (TopOn‘∪ ((𝑘Gen‘𝐽) ↾t 𝐾))) | 
| 25 |  | simpr 484 | . . 3
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → ((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp) | 
| 26 |  | kgenss 23552 | . . . . 5
⊢ (𝐽 ∈ Top → 𝐽 ⊆
(𝑘Gen‘𝐽)) | 
| 27 | 26 | adantr 480 | . . . 4
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → 𝐽
⊆ (𝑘Gen‘𝐽)) | 
| 28 |  | ssrest 23185 | . . . 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 23414 | . . 3
⊢ (((𝐽 ↾t 𝐾) ∈ (TopOn‘∪ ((𝑘Gen‘𝐽) ↾t 𝐾)) ∧ ((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp ∧ (𝐽 ↾t 𝐾) ⊆
((𝑘Gen‘𝐽)
↾t 𝐾))
→ (𝐽
↾t 𝐾)
∈ Comp) | 
| 32 | 24, 25, 29, 31 | syl3anc 1372 | . 2
⊢ ((𝐽 ∈ Top ∧
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp) → (𝐽
↾t 𝐾)
∈ Comp) | 
| 33 | 3, 32 | impbida 800 | 1
⊢ (𝐽 ∈ Top → ((𝐽 ↾t 𝐾) ∈ Comp ↔
((𝑘Gen‘𝐽)
↾t 𝐾)
∈ Comp)) |