![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ishmeo | Structured version Visualization version GIF version |
Description: The predicate F is a homeomorphism between topology 𝐽 and topology 𝐾. Proposition of [BourbakiTop1] p. I.2. (Contributed by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.) |
Ref | Expression |
---|---|
ishmeo | ⊢ (𝐹 ∈ (𝐽Homeo𝐾) ↔ (𝐹 ∈ (𝐽 Cn 𝐾) ∧ ◡𝐹 ∈ (𝐾 Cn 𝐽))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnveq 5630 | . . 3 ⊢ (𝑓 = 𝐹 → ◡𝑓 = ◡𝐹) | |
2 | 1 | eleq1d 2867 | . 2 ⊢ (𝑓 = 𝐹 → (◡𝑓 ∈ (𝐾 Cn 𝐽) ↔ ◡𝐹 ∈ (𝐾 Cn 𝐽))) |
3 | hmeofval 22050 | . 2 ⊢ (𝐽Homeo𝐾) = {𝑓 ∈ (𝐽 Cn 𝐾) ∣ ◡𝑓 ∈ (𝐾 Cn 𝐽)} | |
4 | 2, 3 | elrab2 3621 | 1 ⊢ (𝐹 ∈ (𝐽Homeo𝐾) ↔ (𝐹 ∈ (𝐽 Cn 𝐾) ∧ ◡𝐹 ∈ (𝐾 Cn 𝐽))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 = wceq 1522 ∈ wcel 2081 ◡ccnv 5442 (class class class)co 7016 Cn ccn 21516 Homeochmeo 22045 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3707 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-opab 5025 df-mpt 5042 df-id 5348 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-fv 6233 df-ov 7019 df-oprab 7020 df-mpo 7021 df-map 8258 df-top 21186 df-topon 21203 df-cn 21519 df-hmeo 22047 |
This theorem is referenced by: hmeocn 22052 hmeocnvcn 22053 hmeocnv 22054 hmeores 22063 hmeoco 22064 idhmeo 22065 indishmph 22090 cmphaushmeo 22092 ordthmeo 22094 txhmeo 22095 txswaphmeo 22097 pt1hmeo 22098 ptunhmeo 22100 xkohmeo 22107 qtopf1 22108 qtophmeo 22109 grpinvhmeo 22378 tgplacthmeo 22395 cncfcnvcn 23212 icchmeo 23228 cnrehmeo 23240 cnheiborlem 23241 ismtyhmeo 34634 |
Copyright terms: Public domain | W3C validator |