Step | Hyp | Ref
| Expression |
1 | | hmph 21579 |
. 2
⊢ (𝐽 ≃ 𝐾 ↔ (𝐽Homeo𝐾) ≠ ∅) |
2 | | n0 3931 |
. . 3
⊢ ((𝐽Homeo𝐾) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝐽Homeo𝐾)) |
3 | | hmeocn 21563 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓 ∈ (𝐽 Cn 𝐾)) |
4 | 3 | adantl 482 |
. . . . . . 7
⊢ ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝑓 ∈ (𝐽 Cn 𝐾)) |
5 | | cntop2 21045 |
. . . . . . 7
⊢ (𝑓 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Top) |
7 | | simpll 790 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝐽 ∈ Nrm) |
8 | 4 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑓 ∈ (𝐽 Cn 𝐾)) |
9 | | simprl 794 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑥 ∈ 𝐾) |
10 | | cnima 21069 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ 𝑥 ∈ 𝐾) → (◡𝑓 “ 𝑥) ∈ 𝐽) |
11 | 8, 9, 10 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (◡𝑓 “ 𝑥) ∈ 𝐽) |
12 | | inss1 3833 |
. . . . . . . . . . 11
⊢
((Clsd‘𝐾)
∩ 𝒫 𝑥) ⊆
(Clsd‘𝐾) |
13 | | simprr 796 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥)) |
14 | 12, 13 | sseldi 3601 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ (Clsd‘𝐾)) |
15 | | cnclima 21072 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡𝑓 “ 𝑦) ∈ (Clsd‘𝐽)) |
16 | 8, 14, 15 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (◡𝑓 “ 𝑦) ∈ (Clsd‘𝐽)) |
17 | | inss2 3834 |
. . . . . . . . . . . 12
⊢
((Clsd‘𝐾)
∩ 𝒫 𝑥) ⊆
𝒫 𝑥 |
18 | 17, 13 | sseldi 3601 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ 𝒫 𝑥) |
19 | 18 | elpwid 4170 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ⊆ 𝑥) |
20 | | imass2 5501 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ 𝑥 → (◡𝑓 “ 𝑦) ⊆ (◡𝑓 “ 𝑥)) |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (◡𝑓 “ 𝑦) ⊆ (◡𝑓 “ 𝑥)) |
22 | | nrmsep3 21159 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Nrm ∧ ((◡𝑓 “ 𝑥) ∈ 𝐽 ∧ (◡𝑓 “ 𝑦) ∈ (Clsd‘𝐽) ∧ (◡𝑓 “ 𝑦) ⊆ (◡𝑓 “ 𝑥))) → ∃𝑤 ∈ 𝐽 ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥))) |
23 | 7, 11, 16, 21, 22 | syl13anc 1328 |
. . . . . . . 8
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → ∃𝑤 ∈ 𝐽 ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥))) |
24 | | simpllr 799 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑓 ∈ (𝐽Homeo𝐾)) |
25 | | simprl 794 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑤 ∈ 𝐽) |
26 | | hmeoima 21568 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤 ∈ 𝐽) → (𝑓 “ 𝑤) ∈ 𝐾) |
27 | 24, 25, 26 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → (𝑓 “ 𝑤) ∈ 𝐾) |
28 | | simprrl 804 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → (◡𝑓 “ 𝑦) ⊆ 𝑤) |
29 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝐽 =
∪ 𝐽 |
30 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝐾 =
∪ 𝐾 |
31 | 29, 30 | hmeof1o 21567 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓:∪ 𝐽–1-1-onto→∪ 𝐾) |
32 | 24, 31 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑓:∪ 𝐽–1-1-onto→∪ 𝐾) |
33 | | f1ofun 6139 |
. . . . . . . . . . . 12
⊢ (𝑓:∪
𝐽–1-1-onto→∪ 𝐾
→ Fun 𝑓) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → Fun 𝑓) |
35 | 14 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑦 ∈ (Clsd‘𝐾)) |
36 | 30 | cldss 20833 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (Clsd‘𝐾) → 𝑦 ⊆ ∪ 𝐾) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑦 ⊆ ∪ 𝐾) |
38 | | f1ofo 6144 |
. . . . . . . . . . . . 13
⊢ (𝑓:∪
𝐽–1-1-onto→∪ 𝐾
→ 𝑓:∪ 𝐽–onto→∪ 𝐾) |
39 | | forn 6118 |
. . . . . . . . . . . . 13
⊢ (𝑓:∪
𝐽–onto→∪ 𝐾 → ran 𝑓 = ∪ 𝐾) |
40 | 32, 38, 39 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ran 𝑓 = ∪ 𝐾) |
41 | 37, 40 | sseqtr4d 3642 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑦 ⊆ ran 𝑓) |
42 | | funimass1 5971 |
. . . . . . . . . . 11
⊢ ((Fun
𝑓 ∧ 𝑦 ⊆ ran 𝑓) → ((◡𝑓 “ 𝑦) ⊆ 𝑤 → 𝑦 ⊆ (𝑓 “ 𝑤))) |
43 | 34, 41, 42 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((◡𝑓 “ 𝑦) ⊆ 𝑤 → 𝑦 ⊆ (𝑓 “ 𝑤))) |
44 | 28, 43 | mpd 15 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑦 ⊆ (𝑓 “ 𝑤)) |
45 | | elssuni 4467 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽) |
46 | 45 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑤 ⊆ ∪ 𝐽) |
47 | 29 | hmeocls 21571 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤 ⊆ ∪ 𝐽) → ((cls‘𝐾)‘(𝑓 “ 𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤))) |
48 | 24, 46, 47 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((cls‘𝐾)‘(𝑓 “ 𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤))) |
49 | | simprrr 805 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)) |
50 | | nrmtop 21140 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ Nrm → 𝐽 ∈ Top) |
51 | 50 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝐽 ∈ Top) |
52 | 29 | clsss3 20863 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ 𝑤 ⊆ ∪ 𝐽)
→ ((cls‘𝐽)‘𝑤) ⊆ ∪ 𝐽) |
53 | 51, 46, 52 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ ∪ 𝐽) |
54 | | f1odm 6141 |
. . . . . . . . . . . . . 14
⊢ (𝑓:∪
𝐽–1-1-onto→∪ 𝐾
→ dom 𝑓 = ∪ 𝐽) |
55 | 32, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → dom 𝑓 = ∪ 𝐽) |
56 | 53, 55 | sseqtr4d 3642 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓) |
57 | | funimass3 6333 |
. . . . . . . . . . . 12
⊢ ((Fun
𝑓 ∧ ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥))) |
58 | 34, 56, 57 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥))) |
59 | 49, 58 | mpbird 247 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → (𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥) |
60 | 48, 59 | eqsstrd 3639 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((cls‘𝐾)‘(𝑓 “ 𝑤)) ⊆ 𝑥) |
61 | | sseq2 3627 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑓 “ 𝑤) → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ (𝑓 “ 𝑤))) |
62 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑓 “ 𝑤) → ((cls‘𝐾)‘𝑧) = ((cls‘𝐾)‘(𝑓 “ 𝑤))) |
63 | 62 | sseq1d 3632 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑓 “ 𝑤) → (((cls‘𝐾)‘𝑧) ⊆ 𝑥 ↔ ((cls‘𝐾)‘(𝑓 “ 𝑤)) ⊆ 𝑥)) |
64 | 61, 63 | anbi12d 747 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑓 “ 𝑤) → ((𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥) ↔ (𝑦 ⊆ (𝑓 “ 𝑤) ∧ ((cls‘𝐾)‘(𝑓 “ 𝑤)) ⊆ 𝑥))) |
65 | 64 | rspcev 3309 |
. . . . . . . . 9
⊢ (((𝑓 “ 𝑤) ∈ 𝐾 ∧ (𝑦 ⊆ (𝑓 “ 𝑤) ∧ ((cls‘𝐾)‘(𝑓 “ 𝑤)) ⊆ 𝑥)) → ∃𝑧 ∈ 𝐾 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)) |
66 | 27, 44, 60, 65 | syl12anc 1324 |
. . . . . . . 8
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ∃𝑧 ∈ 𝐾 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)) |
67 | 23, 66 | rexlimddv 3035 |
. . . . . . 7
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → ∃𝑧 ∈ 𝐾 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)) |
68 | 67 | ralrimivva 2971 |
. . . . . 6
⊢ ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥)∃𝑧 ∈ 𝐾 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)) |
69 | | isnrm 21139 |
. . . . . 6
⊢ (𝐾 ∈ Nrm ↔ (𝐾 ∈ Top ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥)∃𝑧 ∈ 𝐾 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))) |
70 | 6, 68, 69 | sylanbrc 698 |
. . . . 5
⊢ ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Nrm) |
71 | 70 | expcom 451 |
. . . 4
⊢ (𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm)) |
72 | 71 | exlimiv 1858 |
. . 3
⊢
(∃𝑓 𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm)) |
73 | 2, 72 | sylbi 207 |
. 2
⊢ ((𝐽Homeo𝐾) ≠ ∅ → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm)) |
74 | 1, 73 | sylbi 207 |
1
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm)) |