Step | Hyp | Ref
| Expression |
1 | | cmphaushmeo.1 |
. . 3
⊢ 𝑋 = ∪
𝐽 |
2 | | cmphaushmeo.2 |
. . 3
⊢ 𝑌 = ∪
𝐾 |
3 | 1, 2 | hmeof1o 22692 |
. 2
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹:𝑋–1-1-onto→𝑌) |
4 | | f1ocnv 6694 |
. . . . . . . 8
⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌–1-1-onto→𝑋) |
5 | | f1of 6682 |
. . . . . . . 8
⊢ (◡𝐹:𝑌–1-1-onto→𝑋 → ◡𝐹:𝑌⟶𝑋) |
6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌⟶𝑋) |
7 | 6 | a1i 11 |
. . . . . 6
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌⟶𝑋)) |
8 | | f1orel 6685 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋–1-1-onto→𝑌 → Rel 𝐹) |
9 | 8 | ad2antll 729 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → Rel 𝐹) |
10 | | dfrel2 6069 |
. . . . . . . . . . 11
⊢ (Rel
𝐹 ↔ ◡◡𝐹 = 𝐹) |
11 | 9, 10 | sylib 221 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → ◡◡𝐹 = 𝐹) |
12 | 11 | imaeq1d 5945 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → (◡◡𝐹 “ 𝑥) = (𝐹 “ 𝑥)) |
13 | | simp2 1139 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Haus) |
14 | 13 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → 𝐾 ∈ Haus) |
15 | | imassrn 5957 |
. . . . . . . . . . 11
⊢ (𝐹 “ 𝑥) ⊆ ran 𝐹 |
16 | | f1ofo 6689 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋–onto→𝑌) |
17 | 16 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → 𝐹:𝑋–onto→𝑌) |
18 | | forn 6657 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋–onto→𝑌 → ran 𝐹 = 𝑌) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → ran 𝐹 = 𝑌) |
20 | 15, 19 | sseqtrid 3969 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → (𝐹 “ 𝑥) ⊆ 𝑌) |
21 | | simpl3 1195 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
22 | | simp1 1138 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Comp) |
23 | 22 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → 𝐽 ∈ Comp) |
24 | | simprl 771 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → 𝑥 ∈ (Clsd‘𝐽)) |
25 | | cmpcld 22330 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Comp ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝑥) ∈ Comp) |
26 | 23, 24, 25 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → (𝐽 ↾t 𝑥) ∈ Comp) |
27 | | imacmp 22325 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ (𝐽 ↾t 𝑥) ∈ Comp) → (𝐾 ↾t (𝐹 “ 𝑥)) ∈ Comp) |
28 | 21, 26, 27 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → (𝐾 ↾t (𝐹 “ 𝑥)) ∈ Comp) |
29 | 2 | hauscmp 22335 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Haus ∧ (𝐹 “ 𝑥) ⊆ 𝑌 ∧ (𝐾 ↾t (𝐹 “ 𝑥)) ∈ Comp) → (𝐹 “ 𝑥) ∈ (Clsd‘𝐾)) |
30 | 14, 20, 28, 29 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → (𝐹 “ 𝑥) ∈ (Clsd‘𝐾)) |
31 | 12, 30 | eqeltrd 2840 |
. . . . . . . 8
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → (◡◡𝐹 “ 𝑥) ∈ (Clsd‘𝐾)) |
32 | 31 | expr 460 |
. . . . . . 7
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝐹:𝑋–1-1-onto→𝑌 → (◡◡𝐹 “ 𝑥) ∈ (Clsd‘𝐾))) |
33 | 32 | ralrimdva 3113 |
. . . . . 6
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹:𝑋–1-1-onto→𝑌 → ∀𝑥 ∈ (Clsd‘𝐽)(◡◡𝐹 “ 𝑥) ∈ (Clsd‘𝐾))) |
34 | 7, 33 | jcad 516 |
. . . . 5
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹:𝑋–1-1-onto→𝑌 → (◡𝐹:𝑌⟶𝑋 ∧ ∀𝑥 ∈ (Clsd‘𝐽)(◡◡𝐹 “ 𝑥) ∈ (Clsd‘𝐾)))) |
35 | | haustop 22259 |
. . . . . . . 8
⊢ (𝐾 ∈ Haus → 𝐾 ∈ Top) |
36 | 13, 35 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Top) |
37 | 2 | toptopon 21845 |
. . . . . . 7
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) |
38 | 36, 37 | sylib 221 |
. . . . . 6
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ (TopOn‘𝑌)) |
39 | | cmptop 22323 |
. . . . . . . 8
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
40 | 22, 39 | syl 17 |
. . . . . . 7
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Top) |
41 | 1 | toptopon 21845 |
. . . . . . 7
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
42 | 40, 41 | sylib 221 |
. . . . . 6
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ (TopOn‘𝑋)) |
43 | | iscncl 22197 |
. . . . . 6
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐽 ∈ (TopOn‘𝑋)) → (◡𝐹 ∈ (𝐾 Cn 𝐽) ↔ (◡𝐹:𝑌⟶𝑋 ∧ ∀𝑥 ∈ (Clsd‘𝐽)(◡◡𝐹 “ 𝑥) ∈ (Clsd‘𝐾)))) |
44 | 38, 42, 43 | syl2anc 587 |
. . . . 5
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (◡𝐹 ∈ (𝐾 Cn 𝐽) ↔ (◡𝐹:𝑌⟶𝑋 ∧ ∀𝑥 ∈ (Clsd‘𝐽)(◡◡𝐹 “ 𝑥) ∈ (Clsd‘𝐾)))) |
45 | 34, 44 | sylibrd 262 |
. . . 4
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹 ∈ (𝐾 Cn 𝐽))) |
46 | | simp3 1140 |
. . . 4
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
47 | 45, 46 | jctild 529 |
. . 3
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹:𝑋–1-1-onto→𝑌 → (𝐹 ∈ (𝐽 Cn 𝐾) ∧ ◡𝐹 ∈ (𝐾 Cn 𝐽)))) |
48 | | ishmeo 22687 |
. . 3
⊢ (𝐹 ∈ (𝐽Homeo𝐾) ↔ (𝐹 ∈ (𝐽 Cn 𝐾) ∧ ◡𝐹 ∈ (𝐾 Cn 𝐽))) |
49 | 47, 48 | syl6ibr 255 |
. 2
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹:𝑋–1-1-onto→𝑌 → 𝐹 ∈ (𝐽Homeo𝐾))) |
50 | 3, 49 | impbid2 229 |
1
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∈ (𝐽Homeo𝐾) ↔ 𝐹:𝑋–1-1-onto→𝑌)) |