Step | Hyp | Ref
| Expression |
1 | | kgenf 21716 |
. . . 4
⊢
𝑘Gen:Top⟶Top |
2 | | ffn 6279 |
. . . 4
⊢
(𝑘Gen:Top⟶Top → 𝑘Gen Fn
Top) |
3 | | fvelrnb 6491 |
. . . 4
⊢
(𝑘Gen Fn Top → (𝐽 ∈ ran 𝑘Gen ↔ ∃𝑗 ∈ Top
(𝑘Gen‘𝑗) =
𝐽)) |
4 | 1, 2, 3 | mp2b 10 |
. . 3
⊢ (𝐽 ∈ ran 𝑘Gen ↔
∃𝑗 ∈ Top
(𝑘Gen‘𝑗) =
𝐽) |
5 | | eqid 2826 |
. . . . . . . . . . . 12
⊢ ∪ 𝑗 =
∪ 𝑗 |
6 | 5 | toptopon 21093 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ Top ↔ 𝑗 ∈ (TopOn‘∪ 𝑗)) |
7 | | kgentopon 21713 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (TopOn‘∪ 𝑗)
→ (𝑘Gen‘𝑗) ∈ (TopOn‘∪ 𝑗)) |
8 | 6, 7 | sylbi 209 |
. . . . . . . . . 10
⊢ (𝑗 ∈ Top →
(𝑘Gen‘𝑗)
∈ (TopOn‘∪ 𝑗)) |
9 | | kgentopon 21713 |
. . . . . . . . . 10
⊢
((𝑘Gen‘𝑗) ∈ (TopOn‘∪ 𝑗)
→ (𝑘Gen‘(𝑘Gen‘𝑗)) ∈ (TopOn‘∪ 𝑗)) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝑗 ∈ Top →
(𝑘Gen‘(𝑘Gen‘𝑗)) ∈ (TopOn‘∪ 𝑗)) |
11 | | toponss 21103 |
. . . . . . . . 9
⊢
(((𝑘Gen‘(𝑘Gen‘𝑗)) ∈ (TopOn‘∪ 𝑗)
∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) → 𝑥 ⊆ ∪ 𝑗) |
12 | 10, 11 | sylan 577 |
. . . . . . . 8
⊢ ((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) → 𝑥 ⊆ ∪ 𝑗) |
13 | | simplr 787 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑗
∧ (𝑗
↾t 𝑘)
∈ Comp)) → 𝑥
∈ (𝑘Gen‘(𝑘Gen‘𝑗))) |
14 | | kgencmp2 21721 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ Top → ((𝑗 ↾t 𝑘) ∈ Comp ↔
((𝑘Gen‘𝑗)
↾t 𝑘)
∈ Comp)) |
15 | 14 | biimpa 470 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ Top ∧ (𝑗 ↾t 𝑘) ∈ Comp) →
((𝑘Gen‘𝑗)
↾t 𝑘)
∈ Comp) |
16 | 15 | ad2ant2rl 757 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑗
∧ (𝑗
↾t 𝑘)
∈ Comp)) → ((𝑘Gen‘𝑗) ↾t 𝑘) ∈ Comp) |
17 | | kgeni 21712 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗)) ∧ ((𝑘Gen‘𝑗) ↾t 𝑘) ∈ Comp) → (𝑥 ∩ 𝑘) ∈ ((𝑘Gen‘𝑗) ↾t 𝑘)) |
18 | 13, 16, 17 | syl2anc 581 |
. . . . . . . . . . 11
⊢ (((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑗
∧ (𝑗
↾t 𝑘)
∈ Comp)) → (𝑥
∩ 𝑘) ∈
((𝑘Gen‘𝑗)
↾t 𝑘)) |
19 | | kgencmp 21720 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ Top ∧ (𝑗 ↾t 𝑘) ∈ Comp) → (𝑗 ↾t 𝑘) = ((𝑘Gen‘𝑗) ↾t 𝑘)) |
20 | 19 | ad2ant2rl 757 |
. . . . . . . . . . 11
⊢ (((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑗
∧ (𝑗
↾t 𝑘)
∈ Comp)) → (𝑗
↾t 𝑘) =
((𝑘Gen‘𝑗)
↾t 𝑘)) |
21 | 18, 20 | eleqtrrd 2910 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑗
∧ (𝑗
↾t 𝑘)
∈ Comp)) → (𝑥
∩ 𝑘) ∈ (𝑗 ↾t 𝑘)) |
22 | 21 | expr 450 |
. . . . . . . . 9
⊢ (((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) ∧ 𝑘 ∈ 𝒫 ∪ 𝑗)
→ ((𝑗
↾t 𝑘)
∈ Comp → (𝑥 ∩
𝑘) ∈ (𝑗 ↾t 𝑘))) |
23 | 22 | ralrimiva 3176 |
. . . . . . . 8
⊢ ((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) → ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))) |
24 | | simpl 476 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) → 𝑗 ∈ Top) |
25 | 24, 6 | sylib 210 |
. . . . . . . . 9
⊢ ((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) → 𝑗 ∈ (TopOn‘∪ 𝑗)) |
26 | | elkgen 21711 |
. . . . . . . . 9
⊢ (𝑗 ∈ (TopOn‘∪ 𝑗)
→ (𝑥 ∈
(𝑘Gen‘𝑗)
↔ (𝑥 ⊆ ∪ 𝑗
∧ ∀𝑘 ∈
𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))))) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
⊢ ((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) → (𝑥 ∈ (𝑘Gen‘𝑗) ↔ (𝑥 ⊆ ∪ 𝑗 ∧ ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))))) |
28 | 12, 23, 27 | mpbir2and 706 |
. . . . . . 7
⊢ ((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) → 𝑥 ∈ (𝑘Gen‘𝑗)) |
29 | 28 | ex 403 |
. . . . . 6
⊢ (𝑗 ∈ Top → (𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗)) → 𝑥 ∈ (𝑘Gen‘𝑗))) |
30 | 29 | ssrdv 3834 |
. . . . 5
⊢ (𝑗 ∈ Top →
(𝑘Gen‘(𝑘Gen‘𝑗)) ⊆ (𝑘Gen‘𝑗)) |
31 | | fveq2 6434 |
. . . . . 6
⊢
((𝑘Gen‘𝑗) = 𝐽 →
(𝑘Gen‘(𝑘Gen‘𝑗)) = (𝑘Gen‘𝐽)) |
32 | | id 22 |
. . . . . 6
⊢
((𝑘Gen‘𝑗) = 𝐽 → (𝑘Gen‘𝑗) = 𝐽) |
33 | 31, 32 | sseq12d 3860 |
. . . . 5
⊢
((𝑘Gen‘𝑗) = 𝐽 →
((𝑘Gen‘(𝑘Gen‘𝑗)) ⊆ (𝑘Gen‘𝑗) ↔
(𝑘Gen‘𝐽)
⊆ 𝐽)) |
34 | 30, 33 | syl5ibcom 237 |
. . . 4
⊢ (𝑗 ∈ Top →
((𝑘Gen‘𝑗) =
𝐽 →
(𝑘Gen‘𝐽)
⊆ 𝐽)) |
35 | 34 | rexlimiv 3237 |
. . 3
⊢
(∃𝑗 ∈ Top
(𝑘Gen‘𝑗) =
𝐽 →
(𝑘Gen‘𝐽)
⊆ 𝐽) |
36 | 4, 35 | sylbi 209 |
. 2
⊢ (𝐽 ∈ ran 𝑘Gen →
(𝑘Gen‘𝐽)
⊆ 𝐽) |
37 | | kgentop 21717 |
. . 3
⊢ (𝐽 ∈ ran 𝑘Gen →
𝐽 ∈
Top) |
38 | | kgenss 21718 |
. . 3
⊢ (𝐽 ∈ Top → 𝐽 ⊆
(𝑘Gen‘𝐽)) |
39 | 37, 38 | syl 17 |
. 2
⊢ (𝐽 ∈ ran 𝑘Gen →
𝐽 ⊆
(𝑘Gen‘𝐽)) |
40 | 36, 39 | eqssd 3845 |
1
⊢ (𝐽 ∈ ran 𝑘Gen →
(𝑘Gen‘𝐽) =
𝐽) |