| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > hmeof1o | Structured version Visualization version GIF version | ||
| Description: A homeomorphism is a 1-1-onto mapping. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 30-May-2014.) |
| Ref | Expression |
|---|---|
| hmeof1o.1 | ⊢ 𝑋 = ∪ 𝐽 |
| hmeof1o.2 | ⊢ 𝑌 = ∪ 𝐾 |
| Ref | Expression |
|---|---|
| hmeof1o | ⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹:𝑋–1-1-onto→𝑌) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hmeocn 23680 | . . 3 ⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹 ∈ (𝐽 Cn 𝐾)) | |
| 2 | cntop1 23160 | . . . . 5 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) | |
| 3 | hmeof1o.1 | . . . . . 6 ⊢ 𝑋 = ∪ 𝐽 | |
| 4 | 3 | toptopon 22837 | . . . . 5 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
| 5 | 2, 4 | sylib 218 | . . . 4 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ (TopOn‘𝑋)) |
| 6 | cntop2 23161 | . . . . 5 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) | |
| 7 | hmeof1o.2 | . . . . . 6 ⊢ 𝑌 = ∪ 𝐾 | |
| 8 | 7 | toptopon 22837 | . . . . 5 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) |
| 9 | 6, 8 | sylib 218 | . . . 4 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ (TopOn‘𝑌)) |
| 10 | 5, 9 | jca 511 | . . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌))) |
| 11 | 1, 10 | syl 17 | . 2 ⊢ (𝐹 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌))) |
| 12 | hmeof1o2 23683 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽Homeo𝐾)) → 𝐹:𝑋–1-1-onto→𝑌) | |
| 13 | 12 | 3expia 1121 | . 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹:𝑋–1-1-onto→𝑌)) |
| 14 | 11, 13 | mpcom 38 | 1 ⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹:𝑋–1-1-onto→𝑌) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∪ cuni 4867 –1-1-onto→wf1o 6498 ‘cfv 6499 (class class class)co 7369 Topctop 22813 TopOnctopon 22830 Cn ccn 23144 Homeochmeo 23673 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rab 3403 df-v 3446 df-sbc 3751 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-ov 7372 df-oprab 7373 df-mpo 7374 df-map 8778 df-top 22814 df-topon 22831 df-cn 23147 df-hmeo 23675 |
| This theorem is referenced by: hmeoopn 23686 hmeocld 23687 hmeontr 23689 hmeoimaf1o 23690 hmeoqtop 23695 haushmphlem 23707 cmphmph 23708 connhmph 23709 reghmph 23713 nrmhmph 23714 hmphdis 23716 hmphen2 23719 cmphaushmeo 23720 txhmeo 23723 tpr2rico 33895 mndpluscn 33909 |
| Copyright terms: Public domain | W3C validator |