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 24078

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 5851	. . 3 ⊢ (𝑓 = 𝐹 → ^◡𝑓 = ^◡𝐹)
2	1	eleq1d 2846	. 2 ⊢ (𝑓 = 𝐹 → (^◡𝑓 ∈ (𝐾 Cn 𝐽) ↔ ^◡𝐹 ∈ (𝐾 Cn 𝐽)))
3		hmeofval 24077	. 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 5650 (class class class)co 7420 Cn ccn 23542 Homeochmeo 24072

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 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751

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 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 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 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-fv 6546 df-ov 7423 df-oprab 7424 df-mpo 7425 df-map 8849 df-top 23212 df-topon 23229 df-cn 23545 df-hmeo 24074

This theorem is used by: hmeocn 24079 hmeocnvcn 24080 hmeocnv 24081 hmeores 24090 hmeoco 24091 idhmeo 24092 indishmph 24117 cmphaushmeo 24119 ordthmeo 24121 txhmeo 24122 txswaphmeo 24124 pt1hmeo 24125 ptunhmeo 24127 xkohmeo 24134 qtopf1 24135 qtophmeo 24136 grpinvhmeo 24405 tgplacthmeo 24422 cncfcnvcn 25246 icchmeo 25262 cnrehmeo 25274 cnheiborlem 25275 ismtyhmeo 38739

W3C validator