Proof of Theorem hmeontr
| Step | Hyp | Ref
| Expression |
| 1 | | hmeocn 23768 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
| 2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
| 3 | | imassrn 6089 |
. . . . . 6
⊢ (𝐹 “ 𝐴) ⊆ ran 𝐹 |
| 4 | | hmeoopn.1 |
. . . . . . . . 9
⊢ 𝑋 = ∪
𝐽 |
| 5 | | eqid 2737 |
. . . . . . . . 9
⊢ ∪ 𝐾 =
∪ 𝐾 |
| 6 | 4, 5 | hmeof1o 23772 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹:𝑋–1-1-onto→∪ 𝐾) |
| 7 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → 𝐹:𝑋–1-1-onto→∪ 𝐾) |
| 8 | | f1ofo 6855 |
. . . . . . 7
⊢ (𝐹:𝑋–1-1-onto→∪ 𝐾
→ 𝐹:𝑋–onto→∪ 𝐾) |
| 9 | | forn 6823 |
. . . . . . 7
⊢ (𝐹:𝑋–onto→∪ 𝐾 → ran 𝐹 = ∪ 𝐾) |
| 10 | 7, 8, 9 | 3syl 18 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → ran 𝐹 = ∪ 𝐾) |
| 11 | 3, 10 | sseqtrid 4026 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐹 “ 𝐴) ⊆ ∪ 𝐾) |
| 12 | 5 | cnntri 23279 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ (𝐹 “ 𝐴) ⊆ ∪ 𝐾) → (◡𝐹 “ ((int‘𝐾)‘(𝐹 “ 𝐴))) ⊆ ((int‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝐴)))) |
| 13 | 2, 11, 12 | syl2anc 584 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → (◡𝐹 “ ((int‘𝐾)‘(𝐹 “ 𝐴))) ⊆ ((int‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝐴)))) |
| 14 | | f1of1 6847 |
. . . . . . 7
⊢ (𝐹:𝑋–1-1-onto→∪ 𝐾
→ 𝐹:𝑋–1-1→∪ 𝐾) |
| 15 | 7, 14 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → 𝐹:𝑋–1-1→∪ 𝐾) |
| 16 | | f1imacnv 6864 |
. . . . . 6
⊢ ((𝐹:𝑋–1-1→∪ 𝐾 ∧ 𝐴 ⊆ 𝑋) → (◡𝐹 “ (𝐹 “ 𝐴)) = 𝐴) |
| 17 | 15, 16 | sylancom 588 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → (◡𝐹 “ (𝐹 “ 𝐴)) = 𝐴) |
| 18 | 17 | fveq2d 6910 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝐴))) = ((int‘𝐽)‘𝐴)) |
| 19 | 13, 18 | sseqtrd 4020 |
. . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → (◡𝐹 “ ((int‘𝐾)‘(𝐹 “ 𝐴))) ⊆ ((int‘𝐽)‘𝐴)) |
| 20 | | f1ofun 6850 |
. . . . 5
⊢ (𝐹:𝑋–1-1-onto→∪ 𝐾
→ Fun 𝐹) |
| 21 | 7, 20 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → Fun 𝐹) |
| 22 | | cntop2 23249 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
| 23 | 2, 22 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → 𝐾 ∈ Top) |
| 24 | 5 | ntrss3 23068 |
. . . . . 6
⊢ ((𝐾 ∈ Top ∧ (𝐹 “ 𝐴) ⊆ ∪ 𝐾) → ((int‘𝐾)‘(𝐹 “ 𝐴)) ⊆ ∪
𝐾) |
| 25 | 23, 11, 24 | syl2anc 584 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐾)‘(𝐹 “ 𝐴)) ⊆ ∪
𝐾) |
| 26 | 25, 10 | sseqtrrd 4021 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐾)‘(𝐹 “ 𝐴)) ⊆ ran 𝐹) |
| 27 | | funimass1 6648 |
. . . 4
⊢ ((Fun
𝐹 ∧ ((int‘𝐾)‘(𝐹 “ 𝐴)) ⊆ ran 𝐹) → ((◡𝐹 “ ((int‘𝐾)‘(𝐹 “ 𝐴))) ⊆ ((int‘𝐽)‘𝐴) → ((int‘𝐾)‘(𝐹 “ 𝐴)) ⊆ (𝐹 “ ((int‘𝐽)‘𝐴)))) |
| 28 | 21, 26, 27 | syl2anc 584 |
. . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → ((◡𝐹 “ ((int‘𝐾)‘(𝐹 “ 𝐴))) ⊆ ((int‘𝐽)‘𝐴) → ((int‘𝐾)‘(𝐹 “ 𝐴)) ⊆ (𝐹 “ ((int‘𝐽)‘𝐴)))) |
| 29 | 19, 28 | mpd 15 |
. 2
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐾)‘(𝐹 “ 𝐴)) ⊆ (𝐹 “ ((int‘𝐽)‘𝐴))) |
| 30 | | hmeocnvcn 23769 |
. . . 4
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → ◡𝐹 ∈ (𝐾 Cn 𝐽)) |
| 31 | 4 | cnntri 23279 |
. . . 4
⊢ ((◡𝐹 ∈ (𝐾 Cn 𝐽) ∧ 𝐴 ⊆ 𝑋) → (◡◡𝐹 “ ((int‘𝐽)‘𝐴)) ⊆ ((int‘𝐾)‘(◡◡𝐹 “ 𝐴))) |
| 32 | 30, 31 | sylan 580 |
. . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → (◡◡𝐹 “ ((int‘𝐽)‘𝐴)) ⊆ ((int‘𝐾)‘(◡◡𝐹 “ 𝐴))) |
| 33 | | imacnvcnv 6226 |
. . 3
⊢ (◡◡𝐹 “ ((int‘𝐽)‘𝐴)) = (𝐹 “ ((int‘𝐽)‘𝐴)) |
| 34 | | imacnvcnv 6226 |
. . . 4
⊢ (◡◡𝐹 “ 𝐴) = (𝐹 “ 𝐴) |
| 35 | 34 | fveq2i 6909 |
. . 3
⊢
((int‘𝐾)‘(◡◡𝐹 “ 𝐴)) = ((int‘𝐾)‘(𝐹 “ 𝐴)) |
| 36 | 32, 33, 35 | 3sstr3g 4036 |
. 2
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐹 “ ((int‘𝐽)‘𝐴)) ⊆ ((int‘𝐾)‘(𝐹 “ 𝐴))) |
| 37 | 29, 36 | eqssd 4001 |
1
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐾)‘(𝐹 “ 𝐴)) = (𝐹 “ ((int‘𝐽)‘𝐴))) |