Step | Hyp | Ref
| Expression |
1 | | kgenf 22681 |
. . . 4
⊢
𝑘Gen:Top⟶Top |
2 | | ffn 6594 |
. . . 4
⊢
(𝑘Gen:Top⟶Top → 𝑘Gen Fn
Top) |
3 | | fvelrnb 6824 |
. . . 4
⊢
(𝑘Gen Fn Top → (𝐽 ∈ ran 𝑘Gen ↔ ∃𝑗 ∈ Top
(𝑘Gen‘𝑗) =
𝐽)) |
4 | 1, 2, 3 | mp2b 10 |
. . 3
⊢ (𝐽 ∈ ran 𝑘Gen ↔
∃𝑗 ∈ Top
(𝑘Gen‘𝑗) =
𝐽) |
5 | | toptopon2 22056 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ Top ↔ 𝑗 ∈ (TopOn‘∪ 𝑗)) |
6 | | kgentopon 22678 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (TopOn‘∪ 𝑗)
→ (𝑘Gen‘𝑗) ∈ (TopOn‘∪ 𝑗)) |
7 | 5, 6 | sylbi 216 |
. . . . . . . . . 10
⊢ (𝑗 ∈ Top →
(𝑘Gen‘𝑗)
∈ (TopOn‘∪ 𝑗)) |
8 | | kgentopon 22678 |
. . . . . . . . . 10
⊢
((𝑘Gen‘𝑗) ∈ (TopOn‘∪ 𝑗)
→ (𝑘Gen‘(𝑘Gen‘𝑗)) ∈ (TopOn‘∪ 𝑗)) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝑗 ∈ Top →
(𝑘Gen‘(𝑘Gen‘𝑗)) ∈ (TopOn‘∪ 𝑗)) |
10 | | toponss 22065 |
. . . . . . . . 9
⊢
(((𝑘Gen‘(𝑘Gen‘𝑗)) ∈ (TopOn‘∪ 𝑗)
∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) → 𝑥 ⊆ ∪ 𝑗) |
11 | 9, 10 | sylan 580 |
. . . . . . . 8
⊢ ((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) → 𝑥 ⊆ ∪ 𝑗) |
12 | | simplr 766 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑗
∧ (𝑗
↾t 𝑘)
∈ Comp)) → 𝑥
∈ (𝑘Gen‘(𝑘Gen‘𝑗))) |
13 | | kgencmp2 22686 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ Top → ((𝑗 ↾t 𝑘) ∈ Comp ↔
((𝑘Gen‘𝑗)
↾t 𝑘)
∈ Comp)) |
14 | 13 | biimpa 477 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ Top ∧ (𝑗 ↾t 𝑘) ∈ Comp) →
((𝑘Gen‘𝑗)
↾t 𝑘)
∈ Comp) |
15 | 14 | ad2ant2rl 746 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑗
∧ (𝑗
↾t 𝑘)
∈ Comp)) → ((𝑘Gen‘𝑗) ↾t 𝑘) ∈ Comp) |
16 | | kgeni 22677 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗)) ∧ ((𝑘Gen‘𝑗) ↾t 𝑘) ∈ Comp) → (𝑥 ∩ 𝑘) ∈ ((𝑘Gen‘𝑗) ↾t 𝑘)) |
17 | 12, 15, 16 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑗
∧ (𝑗
↾t 𝑘)
∈ Comp)) → (𝑥
∩ 𝑘) ∈
((𝑘Gen‘𝑗)
↾t 𝑘)) |
18 | | kgencmp 22685 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ Top ∧ (𝑗 ↾t 𝑘) ∈ Comp) → (𝑗 ↾t 𝑘) = ((𝑘Gen‘𝑗) ↾t 𝑘)) |
19 | 18 | ad2ant2rl 746 |
. . . . . . . . . . 11
⊢ (((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑗
∧ (𝑗
↾t 𝑘)
∈ Comp)) → (𝑗
↾t 𝑘) =
((𝑘Gen‘𝑗)
↾t 𝑘)) |
20 | 17, 19 | eleqtrrd 2842 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑗
∧ (𝑗
↾t 𝑘)
∈ Comp)) → (𝑥
∩ 𝑘) ∈ (𝑗 ↾t 𝑘)) |
21 | 20 | expr 457 |
. . . . . . . . 9
⊢ (((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) ∧ 𝑘 ∈ 𝒫 ∪ 𝑗)
→ ((𝑗
↾t 𝑘)
∈ Comp → (𝑥 ∩
𝑘) ∈ (𝑗 ↾t 𝑘))) |
22 | 21 | ralrimiva 3103 |
. . . . . . . 8
⊢ ((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) → ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))) |
23 | | simpl 483 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) → 𝑗 ∈ Top) |
24 | 23, 5 | sylib 217 |
. . . . . . . . 9
⊢ ((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) → 𝑗 ∈ (TopOn‘∪ 𝑗)) |
25 | | elkgen 22676 |
. . . . . . . . 9
⊢ (𝑗 ∈ (TopOn‘∪ 𝑗)
→ (𝑥 ∈
(𝑘Gen‘𝑗)
↔ (𝑥 ⊆ ∪ 𝑗
∧ ∀𝑘 ∈
𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))))) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ ((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) → (𝑥 ∈ (𝑘Gen‘𝑗) ↔ (𝑥 ⊆ ∪ 𝑗 ∧ ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))))) |
27 | 11, 22, 26 | mpbir2and 710 |
. . . . . . 7
⊢ ((𝑗 ∈ Top ∧ 𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗))) → 𝑥 ∈ (𝑘Gen‘𝑗)) |
28 | 27 | ex 413 |
. . . . . 6
⊢ (𝑗 ∈ Top → (𝑥 ∈
(𝑘Gen‘(𝑘Gen‘𝑗)) → 𝑥 ∈ (𝑘Gen‘𝑗))) |
29 | 28 | ssrdv 3928 |
. . . . 5
⊢ (𝑗 ∈ Top →
(𝑘Gen‘(𝑘Gen‘𝑗)) ⊆ (𝑘Gen‘𝑗)) |
30 | | fveq2 6768 |
. . . . . 6
⊢
((𝑘Gen‘𝑗) = 𝐽 →
(𝑘Gen‘(𝑘Gen‘𝑗)) = (𝑘Gen‘𝐽)) |
31 | | id 22 |
. . . . . 6
⊢
((𝑘Gen‘𝑗) = 𝐽 → (𝑘Gen‘𝑗) = 𝐽) |
32 | 30, 31 | sseq12d 3955 |
. . . . 5
⊢
((𝑘Gen‘𝑗) = 𝐽 →
((𝑘Gen‘(𝑘Gen‘𝑗)) ⊆ (𝑘Gen‘𝑗) ↔
(𝑘Gen‘𝐽)
⊆ 𝐽)) |
33 | 29, 32 | syl5ibcom 244 |
. . . 4
⊢ (𝑗 ∈ Top →
((𝑘Gen‘𝑗) =
𝐽 →
(𝑘Gen‘𝐽)
⊆ 𝐽)) |
34 | 33 | rexlimiv 3208 |
. . 3
⊢
(∃𝑗 ∈ Top
(𝑘Gen‘𝑗) =
𝐽 →
(𝑘Gen‘𝐽)
⊆ 𝐽) |
35 | 4, 34 | sylbi 216 |
. 2
⊢ (𝐽 ∈ ran 𝑘Gen →
(𝑘Gen‘𝐽)
⊆ 𝐽) |
36 | | kgentop 22682 |
. . 3
⊢ (𝐽 ∈ ran 𝑘Gen →
𝐽 ∈
Top) |
37 | | kgenss 22683 |
. . 3
⊢ (𝐽 ∈ Top → 𝐽 ⊆
(𝑘Gen‘𝐽)) |
38 | 36, 37 | syl 17 |
. 2
⊢ (𝐽 ∈ ran 𝑘Gen →
𝐽 ⊆
(𝑘Gen‘𝐽)) |
39 | 35, 38 | eqssd 3939 |
1
⊢ (𝐽 ∈ ran 𝑘Gen →
(𝑘Gen‘𝐽) =
𝐽) |