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 23988

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 5853	. . 3 ⊢ (𝑓 = 𝐹 → ^◡𝑓 = ^◡𝐹)
2	1	eleq1d 2845	. 2 ⊢ (𝑓 = 𝐹 → (^◡𝑓 ∈ (𝐾 Cn 𝐽) ↔ ^◡𝐹 ∈ (𝐾 Cn 𝐽)))
3		hmeofval 23987	. 2 ⊢ (𝐽Homeo𝐾) = {𝑓 ∈ (𝐽 Cn 𝐾) ∣ ^◡𝑓 ∈ (𝐾 Cn 𝐽)}
4	2, 3	elrab2 3649	1 ⊢ (𝐹 ∈ (𝐽Homeo𝐾) ↔ (𝐹 ∈ (𝐽 Cn 𝐾) ∧ ^◡𝐹 ∈ (𝐾 Cn 𝐽)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ^◡ccnv 5654 (class class class)co 7414 Cn ccn 23452 Homeochmeo 23982

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-sbc 3740 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5550 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-fv 6541 df-ov 7417 df-oprab 7418 df-mpo 7419 df-map 8831 df-top 23122 df-topon 23139 df-cn 23455 df-hmeo 23984

This theorem is used by: hmeocn 23989 hmeocnvcn 23990 hmeocnv 23991 hmeores 24000 hmeoco 24001 idhmeo 24002 indishmph 24027 cmphaushmeo 24029 ordthmeo 24031 txhmeo 24032 txswaphmeo 24034 pt1hmeo 24035 ptunhmeo 24037 xkohmeo 24044 qtopf1 24045 qtophmeo 24046 grpinvhmeo 24315 tgplacthmeo 24332 cncfcnvcn 25156 icchmeo 25172 cnrehmeo 25184 cnheiborlem 25185 ismtyhmeo 38558

W3C validator