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 23969

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2146 ^◡ccnv 5662 (class class class)co 7419 Cn ccn 23433 Homeochmeo 23963

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742

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 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-rab 3419 df-v 3459 df-sbc 3747 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-fv 6548 df-ov 7422 df-oprab 7423 df-mpo 7424 df-map 8832 df-top 23103 df-topon 23120 df-cn 23436 df-hmeo 23965

This theorem is used by: hmeocn 23970 hmeocnvcn 23971 hmeocnv 23972 hmeores 23981 hmeoco 23982 idhmeo 23983 indishmph 24008 cmphaushmeo 24010 ordthmeo 24012 txhmeo 24013 txswaphmeo 24015 pt1hmeo 24016 ptunhmeo 24018 xkohmeo 24025 qtopf1 24026 qtophmeo 24027 grpinvhmeo 24296 tgplacthmeo 24313 cncfcnvcn 25137 icchmeo 25153 cnrehmeo 25165 cnheiborlem 25166 ismtyhmeo 38516

W3C validator