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

Definition df-hmeo 21606
Description: Function returning all the homeomorphisms from topology 𝑗 to topology 𝑘. (Contributed by FL, 14-Feb-2007.)
Assertion
Ref Expression
df-hmeo Homeo = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (𝑗 Cn 𝑘) ∣ 𝑓 ∈ (𝑘 Cn 𝑗)})
Distinct variable group:   𝑓,𝑗,𝑘

Detailed syntax breakdown of Definition df-hmeo
StepHypRef Expression
1 chmeo 21604 . 2 class Homeo
2 vj . . 3 setvar 𝑗
3 vk . . 3 setvar 𝑘
4 ctop 20746 . . 3 class Top
5 vf . . . . . . 7 setvar 𝑓
65cv 1522 . . . . . 6 class 𝑓
76ccnv 5142 . . . . 5 class 𝑓
83cv 1522 . . . . . 6 class 𝑘
92cv 1522 . . . . . 6 class 𝑗
10 ccn 21076 . . . . . 6 class Cn
118, 9, 10co 6690 . . . . 5 class (𝑘 Cn 𝑗)
127, 11wcel 2030 . . . 4 wff 𝑓 ∈ (𝑘 Cn 𝑗)
139, 8, 10co 6690 . . . 4 class (𝑗 Cn 𝑘)
1412, 5, 13crab 2945 . . 3 class {𝑓 ∈ (𝑗 Cn 𝑘) ∣ 𝑓 ∈ (𝑘 Cn 𝑗)}
152, 3, 4, 4, 14cmpt2 6692 . 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (𝑗 Cn 𝑘) ∣ 𝑓 ∈ (𝑘 Cn 𝑗)})
161, 15wceq 1523 1 wff Homeo = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (𝑗 Cn 𝑘) ∣ 𝑓 ∈ (𝑘 Cn 𝑗)})
Colors of variables: wff setvar class
This definition is referenced by:  hmeofn  21608  hmeofval  21609
  Copyright terms: Public domain W3C validator