ishmeo - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ishmeo		Structured version Visualization version GIF version

Theorem ishmeo 23925

Description: The predicate F is a homeomorphism between topology 𝐽 and topology 𝐾. Criterion of [BourbakiTop1] p. I.2. (Contributed by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)

**Assertion**
Ref	Expression
ishmeo	⊢ (𝐹 ∈ (𝐽Homeo𝐾) ↔ (𝐹 ∈ (𝐽 Cn 𝐾) ∧ ^◡𝐹 ∈ (𝐾 Cn 𝐽)))

Proof of Theorem ishmeo Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnveq 5859	. . 3 ⊢ (𝑓 = 𝐹 → ^◡𝑓 = ^◡𝐹)
2	1	eleq1d 2848	. 2 ⊢ (𝑓 = 𝐹 → (^◡𝑓 ∈ (𝐾 Cn 𝐽) ↔ ^◡𝐹 ∈ (𝐾 Cn 𝐽)))
3		hmeofval 23924	. 2 ⊢ (𝐽Homeo𝐾) = {𝑓 ∈ (𝐽 Cn 𝐾) ∣ ^◡𝑓 ∈ (𝐾 Cn 𝐽)}
4	2, 3	elrab2 3654	1 ⊢ (𝐹 ∈ (𝐽Homeo𝐾) ↔ (𝐹 ∈ (𝐽 Cn 𝐾) ∧ ^◡𝐹 ∈ (𝐾 Cn 𝐽)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∧ wa 400 = wceq 1570 ∈ wcel 2143 ^◡ccnv 5660 (class class class)co 7410 Cn ccn 23390 Homeochmeo 23919

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-rab 3417 df-v 3457 df-sbc 3745 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-br 5110 df-opab 5174 df-mpt 5193 df-id 5556 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-fv 6544 df-ov 7413 df-oprab 7414 df-mpo 7415 df-map 8822 df-top 23060 df-topon 23077 df-cn 23393 df-hmeo 23921

This theorem is used by: hmeocn 23926 hmeocnvcn 23927 hmeocnv 23928 hmeores 23937 hmeoco 23938 idhmeo 23939 indishmph 23964 cmphaushmeo 23966 ordthmeo 23968 txhmeo 23969 txswaphmeo 23971 pt1hmeo 23972 ptunhmeo 23974 xkohmeo 23981 qtopf1 23982 qtophmeo 23983 grpinvhmeo 24252 tgplacthmeo 24269 cncfcnvcn 25093 icchmeo 25109 cnrehmeo 25121 cnheiborlem 25122 ismtyhmeo 38484

W3C validator