Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 |
2 | | eqid 2622 |
. . . . . . 7
⊢ ∪ 𝐾 =
∪ 𝐾 |
3 | 1, 2 | cnf 21050 |
. . . . . 6
⊢ (𝑓 ∈ (𝐽 Cn 𝐾) → 𝑓:∪ 𝐽⟶∪ 𝐾) |
4 | 3 | adantl 482 |
. . . . 5
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) → 𝑓:∪ 𝐽⟶∪ 𝐾) |
5 | | cnvimass 5485 |
. . . . . . . . 9
⊢ (◡𝑓 “ 𝑥) ⊆ dom 𝑓 |
6 | | fdm 6051 |
. . . . . . . . . . 11
⊢ (𝑓:∪
𝐽⟶∪ 𝐾
→ dom 𝑓 = ∪ 𝐽) |
7 | 4, 6 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) → dom 𝑓 = ∪ 𝐽) |
8 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) → dom 𝑓 = ∪ 𝐽) |
9 | 5, 8 | syl5sseq 3653 |
. . . . . . . 8
⊢ ((((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) → (◡𝑓 “ 𝑥) ⊆ ∪ 𝐽) |
10 | | cnvresima 5623 |
. . . . . . . . . . . 12
⊢ (◡(𝑓 ↾ 𝑦) “ (𝑥 ∩ (𝑓 “ 𝑦))) = ((◡𝑓 “ (𝑥 ∩ (𝑓 “ 𝑦))) ∩ 𝑦) |
11 | 4 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → 𝑓:∪ 𝐽⟶∪ 𝐾) |
12 | | ffun 6048 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:∪
𝐽⟶∪ 𝐾
→ Fun 𝑓) |
13 | | inpreima 6342 |
. . . . . . . . . . . . . . 15
⊢ (Fun
𝑓 → (◡𝑓 “ (𝑥 ∩ (𝑓 “ 𝑦))) = ((◡𝑓 “ 𝑥) ∩ (◡𝑓 “ (𝑓 “ 𝑦)))) |
14 | 11, 12, 13 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → (◡𝑓 “ (𝑥 ∩ (𝑓 “ 𝑦))) = ((◡𝑓 “ 𝑥) ∩ (◡𝑓 “ (𝑓 “ 𝑦)))) |
15 | 14 | ineq1d 3813 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → ((◡𝑓 “ (𝑥 ∩ (𝑓 “ 𝑦))) ∩ 𝑦) = (((◡𝑓 “ 𝑥) ∩ (◡𝑓 “ (𝑓 “ 𝑦))) ∩ 𝑦)) |
16 | | in32 3825 |
. . . . . . . . . . . . . 14
⊢ (((◡𝑓 “ 𝑥) ∩ (◡𝑓 “ (𝑓 “ 𝑦))) ∩ 𝑦) = (((◡𝑓 “ 𝑥) ∩ 𝑦) ∩ (◡𝑓 “ (𝑓 “ 𝑦))) |
17 | | ssrin 3838 |
. . . . . . . . . . . . . . . . . 18
⊢ ((◡𝑓 “ 𝑥) ⊆ dom 𝑓 → ((◡𝑓 “ 𝑥) ∩ 𝑦) ⊆ (dom 𝑓 ∩ 𝑦)) |
18 | 5, 17 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝑓 “ 𝑥) ∩ 𝑦) ⊆ (dom 𝑓 ∩ 𝑦) |
19 | | dminss 5547 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
𝑓 ∩ 𝑦) ⊆ (◡𝑓 “ (𝑓 “ 𝑦)) |
20 | 18, 19 | sstri 3612 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝑓 “ 𝑥) ∩ 𝑦) ⊆ (◡𝑓 “ (𝑓 “ 𝑦)) |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → ((◡𝑓 “ 𝑥) ∩ 𝑦) ⊆ (◡𝑓 “ (𝑓 “ 𝑦))) |
22 | | df-ss 3588 |
. . . . . . . . . . . . . . 15
⊢ (((◡𝑓 “ 𝑥) ∩ 𝑦) ⊆ (◡𝑓 “ (𝑓 “ 𝑦)) ↔ (((◡𝑓 “ 𝑥) ∩ 𝑦) ∩ (◡𝑓 “ (𝑓 “ 𝑦))) = ((◡𝑓 “ 𝑥) ∩ 𝑦)) |
23 | 21, 22 | sylib 208 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → (((◡𝑓 “ 𝑥) ∩ 𝑦) ∩ (◡𝑓 “ (𝑓 “ 𝑦))) = ((◡𝑓 “ 𝑥) ∩ 𝑦)) |
24 | 16, 23 | syl5eq 2668 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → (((◡𝑓 “ 𝑥) ∩ (◡𝑓 “ (𝑓 “ 𝑦))) ∩ 𝑦) = ((◡𝑓 “ 𝑥) ∩ 𝑦)) |
25 | 15, 24 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → ((◡𝑓 “ (𝑥 ∩ (𝑓 “ 𝑦))) ∩ 𝑦) = ((◡𝑓 “ 𝑥) ∩ 𝑦)) |
26 | 10, 25 | syl5eq 2668 |
. . . . . . . . . . 11
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → (◡(𝑓 ↾ 𝑦) “ (𝑥 ∩ (𝑓 “ 𝑦))) = ((◡𝑓 “ 𝑥) ∩ 𝑦)) |
27 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) → 𝑓 ∈ (𝐽 Cn 𝐾)) |
28 | 27 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → 𝑓
∈ (𝐽 Cn 𝐾)) |
29 | | elpwi 4168 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝒫 ∪ 𝐽
→ 𝑦 ⊆ ∪ 𝐽) |
30 | 29 | ad2antrl 764 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → 𝑦
⊆ ∪ 𝐽) |
31 | 1 | cnrest 21089 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ 𝑦 ⊆ ∪ 𝐽) → (𝑓 ↾ 𝑦) ∈ ((𝐽 ↾t 𝑦) Cn 𝐾)) |
32 | 28, 30, 31 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → (𝑓
↾ 𝑦) ∈ ((𝐽 ↾t 𝑦) Cn 𝐾)) |
33 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) → 𝐾 ∈ Top) |
34 | 33 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → 𝐾
∈ Top) |
35 | 2 | toptopon 20722 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
36 | 34, 35 | sylib 208 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → 𝐾
∈ (TopOn‘∪ 𝐾)) |
37 | | df-ima 5127 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 “ 𝑦) = ran (𝑓 ↾ 𝑦) |
38 | 37 | eqimss2i 3660 |
. . . . . . . . . . . . . . 15
⊢ ran
(𝑓 ↾ 𝑦) ⊆ (𝑓 “ 𝑦) |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → ran (𝑓
↾ 𝑦) ⊆ (𝑓 “ 𝑦)) |
40 | | imassrn 5477 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 “ 𝑦) ⊆ ran 𝑓 |
41 | | frn 6053 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:∪
𝐽⟶∪ 𝐾
→ ran 𝑓 ⊆ ∪ 𝐾) |
42 | 11, 41 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → ran 𝑓
⊆ ∪ 𝐾) |
43 | 40, 42 | syl5ss 3614 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → (𝑓
“ 𝑦) ⊆ ∪ 𝐾) |
44 | | cnrest2 21090 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ ran (𝑓 ↾ 𝑦) ⊆ (𝑓 “ 𝑦) ∧ (𝑓 “ 𝑦) ⊆ ∪ 𝐾) → ((𝑓 ↾ 𝑦) ∈ ((𝐽 ↾t 𝑦) Cn 𝐾) ↔ (𝑓 ↾ 𝑦) ∈ ((𝐽 ↾t 𝑦) Cn (𝐾 ↾t (𝑓 “ 𝑦))))) |
45 | 36, 39, 43, 44 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → ((𝑓
↾ 𝑦) ∈ ((𝐽 ↾t 𝑦) Cn 𝐾) ↔ (𝑓 ↾ 𝑦) ∈ ((𝐽 ↾t 𝑦) Cn (𝐾 ↾t (𝑓 “ 𝑦))))) |
46 | 32, 45 | mpbid 222 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → (𝑓
↾ 𝑦) ∈ ((𝐽 ↾t 𝑦) Cn (𝐾 ↾t (𝑓 “ 𝑦)))) |
47 | | simplr 792 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → 𝑥
∈ (𝑘Gen‘𝐾)) |
48 | | simprr 796 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → (𝐽
↾t 𝑦)
∈ Comp) |
49 | | imacmp 21200 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ (𝐽 ↾t 𝑦) ∈ Comp) → (𝐾 ↾t (𝑓 “ 𝑦)) ∈ Comp) |
50 | 28, 48, 49 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → (𝐾
↾t (𝑓
“ 𝑦)) ∈
Comp) |
51 | | kgeni 21340 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈
(𝑘Gen‘𝐾)
∧ (𝐾
↾t (𝑓
“ 𝑦)) ∈ Comp)
→ (𝑥 ∩ (𝑓 “ 𝑦)) ∈ (𝐾 ↾t (𝑓 “ 𝑦))) |
52 | 47, 50, 51 | syl2anc 693 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → (𝑥
∩ (𝑓 “ 𝑦)) ∈ (𝐾 ↾t (𝑓 “ 𝑦))) |
53 | | cnima 21069 |
. . . . . . . . . . . 12
⊢ (((𝑓 ↾ 𝑦) ∈ ((𝐽 ↾t 𝑦) Cn (𝐾 ↾t (𝑓 “ 𝑦))) ∧ (𝑥 ∩ (𝑓 “ 𝑦)) ∈ (𝐾 ↾t (𝑓 “ 𝑦))) → (◡(𝑓 ↾ 𝑦) “ (𝑥 ∩ (𝑓 “ 𝑦))) ∈ (𝐽 ↾t 𝑦)) |
54 | 46, 52, 53 | syl2anc 693 |
. . . . . . . . . . 11
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → (◡(𝑓 ↾ 𝑦) “ (𝑥 ∩ (𝑓 “ 𝑦))) ∈ (𝐽 ↾t 𝑦)) |
55 | 26, 54 | eqeltrrd 2702 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ (𝑦 ∈ 𝒫 ∪ 𝐽
∧ (𝐽
↾t 𝑦)
∈ Comp)) → ((◡𝑓 “ 𝑥) ∩ 𝑦) ∈ (𝐽 ↾t 𝑦)) |
56 | 55 | expr 643 |
. . . . . . . . 9
⊢
(((((𝐽 ∈ ran
𝑘Gen ∧ 𝐾 ∈
Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) ∧ 𝑦 ∈ 𝒫 ∪ 𝐽)
→ ((𝐽
↾t 𝑦)
∈ Comp → ((◡𝑓 “ 𝑥) ∩ 𝑦) ∈ (𝐽 ↾t 𝑦))) |
57 | 56 | ralrimiva 2966 |
. . . . . . . 8
⊢ ((((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) → ∀𝑦 ∈ 𝒫 ∪ 𝐽((𝐽 ↾t 𝑦) ∈ Comp → ((◡𝑓 “ 𝑥) ∩ 𝑦) ∈ (𝐽 ↾t 𝑦))) |
58 | | kgentop 21345 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ ran 𝑘Gen →
𝐽 ∈
Top) |
59 | 58 | ad3antrrr 766 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) → 𝐽 ∈ Top) |
60 | 1 | toptopon 20722 |
. . . . . . . . . 10
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
61 | 59, 60 | sylib 208 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
62 | | elkgen 21339 |
. . . . . . . . 9
⊢ (𝐽 ∈ (TopOn‘∪ 𝐽)
→ ((◡𝑓 “ 𝑥) ∈ (𝑘Gen‘𝐽) ↔ ((◡𝑓 “ 𝑥) ⊆ ∪ 𝐽 ∧ ∀𝑦 ∈ 𝒫 ∪ 𝐽((𝐽 ↾t 𝑦) ∈ Comp → ((◡𝑓 “ 𝑥) ∩ 𝑦) ∈ (𝐽 ↾t 𝑦))))) |
63 | 61, 62 | syl 17 |
. . . . . . . 8
⊢ ((((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) → ((◡𝑓 “ 𝑥) ∈ (𝑘Gen‘𝐽) ↔ ((◡𝑓 “ 𝑥) ⊆ ∪ 𝐽 ∧ ∀𝑦 ∈ 𝒫 ∪ 𝐽((𝐽 ↾t 𝑦) ∈ Comp → ((◡𝑓 “ 𝑥) ∩ 𝑦) ∈ (𝐽 ↾t 𝑦))))) |
64 | 9, 57, 63 | mpbir2and 957 |
. . . . . . 7
⊢ ((((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) → (◡𝑓 “ 𝑥) ∈ (𝑘Gen‘𝐽)) |
65 | | kgenidm 21350 |
. . . . . . . 8
⊢ (𝐽 ∈ ran 𝑘Gen →
(𝑘Gen‘𝐽) =
𝐽) |
66 | 65 | ad3antrrr 766 |
. . . . . . 7
⊢ ((((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) → (𝑘Gen‘𝐽) = 𝐽) |
67 | 64, 66 | eleqtrd 2703 |
. . . . . 6
⊢ ((((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝑘Gen‘𝐾)) → (◡𝑓 “ 𝑥) ∈ 𝐽) |
68 | 67 | ralrimiva 2966 |
. . . . 5
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) → ∀𝑥 ∈ (𝑘Gen‘𝐾)(◡𝑓 “ 𝑥) ∈ 𝐽) |
69 | 58, 60 | sylib 208 |
. . . . . . 7
⊢ (𝐽 ∈ ran 𝑘Gen →
𝐽 ∈ (TopOn‘∪ 𝐽)) |
70 | | kgentopon 21341 |
. . . . . . . 8
⊢ (𝐾 ∈ (TopOn‘∪ 𝐾)
→ (𝑘Gen‘𝐾) ∈ (TopOn‘∪ 𝐾)) |
71 | 35, 70 | sylbi 207 |
. . . . . . 7
⊢ (𝐾 ∈ Top →
(𝑘Gen‘𝐾)
∈ (TopOn‘∪ 𝐾)) |
72 | | iscn 21039 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ (𝑘Gen‘𝐾) ∈ (TopOn‘∪ 𝐾))
→ (𝑓 ∈ (𝐽 Cn (𝑘Gen‘𝐾)) ↔ (𝑓:∪ 𝐽⟶∪ 𝐾
∧ ∀𝑥 ∈
(𝑘Gen‘𝐾)(◡𝑓 “ 𝑥) ∈ 𝐽))) |
73 | 69, 71, 72 | syl2an 494 |
. . . . . 6
⊢ ((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) → (𝑓 ∈ (𝐽 Cn (𝑘Gen‘𝐾)) ↔ (𝑓:∪ 𝐽⟶∪ 𝐾
∧ ∀𝑥 ∈
(𝑘Gen‘𝐾)(◡𝑓 “ 𝑥) ∈ 𝐽))) |
74 | 73 | adantr 481 |
. . . . 5
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) → (𝑓 ∈ (𝐽 Cn (𝑘Gen‘𝐾)) ↔ (𝑓:∪ 𝐽⟶∪ 𝐾
∧ ∀𝑥 ∈
(𝑘Gen‘𝐾)(◡𝑓 “ 𝑥) ∈ 𝐽))) |
75 | 4, 68, 74 | mpbir2and 957 |
. . . 4
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) ∧ 𝑓 ∈ (𝐽 Cn 𝐾)) → 𝑓 ∈ (𝐽 Cn (𝑘Gen‘𝐾))) |
76 | 75 | ex 450 |
. . 3
⊢ ((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) → (𝑓 ∈ (𝐽 Cn 𝐾) → 𝑓 ∈ (𝐽 Cn (𝑘Gen‘𝐾)))) |
77 | 76 | ssrdv 3609 |
. 2
⊢ ((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) → (𝐽 Cn 𝐾) ⊆ (𝐽 Cn (𝑘Gen‘𝐾))) |
78 | 71 | adantl 482 |
. . . 4
⊢ ((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) →
(𝑘Gen‘𝐾)
∈ (TopOn‘∪ 𝐾)) |
79 | | toponcom 20732 |
. . . 4
⊢ ((𝐾 ∈ Top ∧
(𝑘Gen‘𝐾)
∈ (TopOn‘∪ 𝐾)) → 𝐾 ∈ (TopOn‘∪ (𝑘Gen‘𝐾))) |
80 | 33, 78, 79 | syl2anc 693 |
. . 3
⊢ ((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) → 𝐾 ∈ (TopOn‘∪ (𝑘Gen‘𝐾))) |
81 | | kgenss 21346 |
. . . 4
⊢ (𝐾 ∈ Top → 𝐾 ⊆
(𝑘Gen‘𝐾)) |
82 | 81 | adantl 482 |
. . 3
⊢ ((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) → 𝐾 ⊆
(𝑘Gen‘𝐾)) |
83 | | eqid 2622 |
. . . 4
⊢ ∪ (𝑘Gen‘𝐾) = ∪
(𝑘Gen‘𝐾) |
84 | 83 | cnss2 21081 |
. . 3
⊢ ((𝐾 ∈ (TopOn‘∪ (𝑘Gen‘𝐾)) ∧ 𝐾 ⊆ (𝑘Gen‘𝐾)) → (𝐽 Cn (𝑘Gen‘𝐾)) ⊆ (𝐽 Cn 𝐾)) |
85 | 80, 82, 84 | syl2anc 693 |
. 2
⊢ ((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) → (𝐽 Cn (𝑘Gen‘𝐾)) ⊆ (𝐽 Cn 𝐾)) |
86 | 77, 85 | eqssd 3620 |
1
⊢ ((𝐽 ∈ ran 𝑘Gen ∧
𝐾 ∈ Top) → (𝐽 Cn 𝐾) = (𝐽 Cn (𝑘Gen‘𝐾))) |