Step | Hyp | Ref
| Expression |
1 | | topontop 20541 |
. . 3
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
2 | 1 | adantr 480 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) → 𝐽 ∈ Top) |
3 | | simplr 788 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → (KQ‘𝐽) ∈ Nrm) |
4 | | simpll 786 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝐽 ∈ (TopOn‘𝑋)) |
5 | | simprl 790 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝑧 ∈ 𝐽) |
6 | | kqval.2 |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) |
7 | 6 | kqopn 21347 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽) → (𝐹 “ 𝑧) ∈ (KQ‘𝐽)) |
8 | 4, 5, 7 | syl2anc 691 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → (𝐹 “ 𝑧) ∈ (KQ‘𝐽)) |
9 | | inss1 3795 |
. . . . . . 7
⊢
((Clsd‘𝐽)
∩ 𝒫 𝑧) ⊆
(Clsd‘𝐽) |
10 | | simprr 792 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧)) |
11 | 9, 10 | sseldi 3566 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝑤 ∈ (Clsd‘𝐽)) |
12 | 6 | kqcld 21348 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑤 ∈ (Clsd‘𝐽)) → (𝐹 “ 𝑤) ∈ (Clsd‘(KQ‘𝐽))) |
13 | 4, 11, 12 | syl2anc 691 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → (𝐹 “ 𝑤) ∈ (Clsd‘(KQ‘𝐽))) |
14 | | inss2 3796 |
. . . . . . 7
⊢
((Clsd‘𝐽)
∩ 𝒫 𝑧) ⊆
𝒫 𝑧 |
15 | 14, 10 | sseldi 3566 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → 𝑤 ∈ 𝒫 𝑧) |
16 | | elpwi 4117 |
. . . . . 6
⊢ (𝑤 ∈ 𝒫 𝑧 → 𝑤 ⊆ 𝑧) |
17 | | imass2 5420 |
. . . . . 6
⊢ (𝑤 ⊆ 𝑧 → (𝐹 “ 𝑤) ⊆ (𝐹 “ 𝑧)) |
18 | 15, 16, 17 | 3syl 18 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → (𝐹 “ 𝑤) ⊆ (𝐹 “ 𝑧)) |
19 | | nrmsep3 20969 |
. . . . 5
⊢
(((KQ‘𝐽)
∈ Nrm ∧ ((𝐹
“ 𝑧) ∈
(KQ‘𝐽) ∧ (𝐹 “ 𝑤) ∈ (Clsd‘(KQ‘𝐽)) ∧ (𝐹 “ 𝑤) ⊆ (𝐹 “ 𝑧))) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧))) |
20 | 3, 8, 13, 18, 19 | syl13anc 1320 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → ∃𝑚 ∈ (KQ‘𝐽)((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧))) |
21 | | simplll 794 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝐽 ∈ (TopOn‘𝑋)) |
22 | 6 | kqid 21341 |
. . . . . . 7
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽))) |
23 | 21, 22 | syl 17 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽))) |
24 | | simprl 790 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑚 ∈ (KQ‘𝐽)) |
25 | | cnima 20879 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑚 ∈ (KQ‘𝐽)) → (◡𝐹 “ 𝑚) ∈ 𝐽) |
26 | 23, 24, 25 | syl2anc 691 |
. . . . 5
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (◡𝐹 “ 𝑚) ∈ 𝐽) |
27 | | simprrl 800 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (𝐹 “ 𝑤) ⊆ 𝑚) |
28 | 6 | kqffn 21338 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋) |
29 | | fnfun 5902 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑋 → Fun 𝐹) |
30 | 21, 28, 29 | 3syl 18 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → Fun 𝐹) |
31 | 11 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ∈ (Clsd‘𝐽)) |
32 | | eqid 2610 |
. . . . . . . . . 10
⊢ ∪ 𝐽 =
∪ 𝐽 |
33 | 32 | cldss 20643 |
. . . . . . . . 9
⊢ (𝑤 ∈ (Clsd‘𝐽) → 𝑤 ⊆ ∪ 𝐽) |
34 | 31, 33 | syl 17 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ⊆ ∪ 𝐽) |
35 | | fndm 5904 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋) |
36 | 21, 28, 35 | 3syl 18 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → dom 𝐹 = 𝑋) |
37 | | toponuni 20542 |
. . . . . . . . . 10
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
38 | 21, 37 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑋 = ∪ 𝐽) |
39 | 36, 38 | eqtrd 2644 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → dom 𝐹 = ∪ 𝐽) |
40 | 34, 39 | sseqtr4d 3605 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ⊆ dom 𝐹) |
41 | | funimass3 6241 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑤 ⊆ dom 𝐹) → ((𝐹 “ 𝑤) ⊆ 𝑚 ↔ 𝑤 ⊆ (◡𝐹 “ 𝑚))) |
42 | 30, 40, 41 | syl2anc 691 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ((𝐹 “ 𝑤) ⊆ 𝑚 ↔ 𝑤 ⊆ (◡𝐹 “ 𝑚))) |
43 | 27, 42 | mpbid 221 |
. . . . 5
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑤 ⊆ (◡𝐹 “ 𝑚)) |
44 | 6 | kqtopon 21340 |
. . . . . . . . . 10
⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹)) |
45 | | topontop 20541 |
. . . . . . . . . 10
⊢
((KQ‘𝐽) ∈
(TopOn‘ran 𝐹) →
(KQ‘𝐽) ∈
Top) |
46 | 21, 44, 45 | 3syl 18 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (KQ‘𝐽) ∈ Top) |
47 | | elssuni 4403 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (KQ‘𝐽) → 𝑚 ⊆ ∪
(KQ‘𝐽)) |
48 | 47 | ad2antrl 760 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑚 ⊆ ∪
(KQ‘𝐽)) |
49 | | eqid 2610 |
. . . . . . . . . 10
⊢ ∪ (KQ‘𝐽) = ∪
(KQ‘𝐽) |
50 | 49 | clscld 20661 |
. . . . . . . . 9
⊢
(((KQ‘𝐽)
∈ Top ∧ 𝑚 ⊆
∪ (KQ‘𝐽)) → ((cls‘(KQ‘𝐽))‘𝑚) ∈ (Clsd‘(KQ‘𝐽))) |
51 | 46, 48, 50 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ((cls‘(KQ‘𝐽))‘𝑚) ∈ (Clsd‘(KQ‘𝐽))) |
52 | | cnclima 20882 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ ((cls‘(KQ‘𝐽))‘𝑚) ∈ (Clsd‘(KQ‘𝐽))) → (◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ∈ (Clsd‘𝐽)) |
53 | 23, 51, 52 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ∈ (Clsd‘𝐽)) |
54 | 49 | sscls 20670 |
. . . . . . . . 9
⊢
(((KQ‘𝐽)
∈ Top ∧ 𝑚 ⊆
∪ (KQ‘𝐽)) → 𝑚 ⊆ ((cls‘(KQ‘𝐽))‘𝑚)) |
55 | 46, 48, 54 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑚 ⊆ ((cls‘(KQ‘𝐽))‘𝑚)) |
56 | | imass2 5420 |
. . . . . . . 8
⊢ (𝑚 ⊆
((cls‘(KQ‘𝐽))‘𝑚) → (◡𝐹 “ 𝑚) ⊆ (◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚))) |
57 | 55, 56 | syl 17 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (◡𝐹 “ 𝑚) ⊆ (◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚))) |
58 | 32 | clsss2 20686 |
. . . . . . 7
⊢ (((◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ∈ (Clsd‘𝐽) ∧ (◡𝐹 “ 𝑚) ⊆ (◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚))) → ((cls‘𝐽)‘(◡𝐹 “ 𝑚)) ⊆ (◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚))) |
59 | 53, 57, 58 | syl2anc 691 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ((cls‘𝐽)‘(◡𝐹 “ 𝑚)) ⊆ (◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚))) |
60 | | simprrr 801 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)) |
61 | | imass2 5420 |
. . . . . . . 8
⊢
(((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧) → (◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ⊆ (◡𝐹 “ (𝐹 “ 𝑧))) |
62 | 60, 61 | syl 17 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ⊆ (◡𝐹 “ (𝐹 “ 𝑧))) |
63 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → 𝑧 ∈ 𝐽) |
64 | 6 | kqsat 21344 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝐽) → (◡𝐹 “ (𝐹 “ 𝑧)) = 𝑧) |
65 | 21, 63, 64 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (◡𝐹 “ (𝐹 “ 𝑧)) = 𝑧) |
66 | 62, 65 | sseqtrd 3604 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → (◡𝐹 “ ((cls‘(KQ‘𝐽))‘𝑚)) ⊆ 𝑧) |
67 | 59, 66 | sstrd 3578 |
. . . . 5
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ((cls‘𝐽)‘(◡𝐹 “ 𝑚)) ⊆ 𝑧) |
68 | | sseq2 3590 |
. . . . . . 7
⊢ (𝑢 = (◡𝐹 “ 𝑚) → (𝑤 ⊆ 𝑢 ↔ 𝑤 ⊆ (◡𝐹 “ 𝑚))) |
69 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑢 = (◡𝐹 “ 𝑚) → ((cls‘𝐽)‘𝑢) = ((cls‘𝐽)‘(◡𝐹 “ 𝑚))) |
70 | 69 | sseq1d 3595 |
. . . . . . 7
⊢ (𝑢 = (◡𝐹 “ 𝑚) → (((cls‘𝐽)‘𝑢) ⊆ 𝑧 ↔ ((cls‘𝐽)‘(◡𝐹 “ 𝑚)) ⊆ 𝑧)) |
71 | 68, 70 | anbi12d 743 |
. . . . . 6
⊢ (𝑢 = (◡𝐹 “ 𝑚) → ((𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧) ↔ (𝑤 ⊆ (◡𝐹 “ 𝑚) ∧ ((cls‘𝐽)‘(◡𝐹 “ 𝑚)) ⊆ 𝑧))) |
72 | 71 | rspcev 3282 |
. . . . 5
⊢ (((◡𝐹 “ 𝑚) ∈ 𝐽 ∧ (𝑤 ⊆ (◡𝐹 “ 𝑚) ∧ ((cls‘𝐽)‘(◡𝐹 “ 𝑚)) ⊆ 𝑧)) → ∃𝑢 ∈ 𝐽 (𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧)) |
73 | 26, 43, 67, 72 | syl12anc 1316 |
. . . 4
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) ∧ (𝑚 ∈ (KQ‘𝐽) ∧ ((𝐹 “ 𝑤) ⊆ 𝑚 ∧ ((cls‘(KQ‘𝐽))‘𝑚) ⊆ (𝐹 “ 𝑧)))) → ∃𝑢 ∈ 𝐽 (𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧)) |
74 | 20, 73 | rexlimddv 3017 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) ∧ (𝑧 ∈ 𝐽 ∧ 𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧))) → ∃𝑢 ∈ 𝐽 (𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧)) |
75 | 74 | ralrimivva 2954 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) →
∀𝑧 ∈ 𝐽 ∀𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧)∃𝑢 ∈ 𝐽 (𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧)) |
76 | | isnrm 20949 |
. 2
⊢ (𝐽 ∈ Nrm ↔ (𝐽 ∈ Top ∧ ∀𝑧 ∈ 𝐽 ∀𝑤 ∈ ((Clsd‘𝐽) ∩ 𝒫 𝑧)∃𝑢 ∈ 𝐽 (𝑤 ⊆ 𝑢 ∧ ((cls‘𝐽)‘𝑢) ⊆ 𝑧))) |
77 | 2, 75, 76 | sylanbrc 695 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) → 𝐽 ∈ Nrm) |