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

Theorem cnheiborlem 22509
Description: Lemma for cnheibor 22510. (Contributed by Mario Carneiro, 14-Sep-2014.)
Hypotheses
Ref Expression
cnheibor.2 𝐽 = (TopOpen‘ℂfld)
cnheibor.3 𝑇 = (𝐽t 𝑋)
cnheibor.4 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))
cnheibor.5 𝑌 = (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))
Assertion
Ref Expression
cnheiborlem ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑇 ∈ Comp)
Distinct variable groups:   𝑥,𝑦,𝑧   𝑧,𝐹   𝑧,𝑅   𝑥,𝑇,𝑦,𝑧   𝑥,𝐽,𝑦,𝑧   𝑥,𝑋,𝑦,𝑧
Allowed substitution hints:   𝑅(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝑌(𝑥,𝑦,𝑧)

Proof of Theorem cnheiborlem
Dummy variable 𝑢 is distinct from all other variables.
StepHypRef Expression
1 cnheibor.2 . . . . 5 𝐽 = (TopOpen‘ℂfld)
21cnfldtop 22345 . . . 4 𝐽 ∈ Top
3 cnheibor.4 . . . . . . . . . 10 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))
43cnref1o 11662 . . . . . . . . 9 𝐹:(ℝ × ℝ)–1-1-onto→ℂ
5 f1ofn 6036 . . . . . . . . 9 (𝐹:(ℝ × ℝ)–1-1-onto→ℂ → 𝐹 Fn (ℝ × ℝ))
6 elpreima 6230 . . . . . . . . 9 (𝐹 Fn (ℝ × ℝ) → (𝑢 ∈ (𝐹𝑋) ↔ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)))
74, 5, 6mp2b 10 . . . . . . . 8 (𝑢 ∈ (𝐹𝑋) ↔ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋))
8 1st2nd2 7074 . . . . . . . . . . 11 (𝑢 ∈ (ℝ × ℝ) → 𝑢 = ⟨(1st𝑢), (2nd𝑢)⟩)
98ad2antrl 760 . . . . . . . . . 10 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → 𝑢 = ⟨(1st𝑢), (2nd𝑢)⟩)
10 xp1st 7067 . . . . . . . . . . . . 13 (𝑢 ∈ (ℝ × ℝ) → (1st𝑢) ∈ ℝ)
1110ad2antrl 760 . . . . . . . . . . . 12 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (1st𝑢) ∈ ℝ)
1211recnd 9925 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (1st𝑢) ∈ ℂ)
1312abscld 13972 . . . . . . . . . . . . . . 15 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(1st𝑢)) ∈ ℝ)
141cnfldtopon 22344 . . . . . . . . . . . . . . . . . . . . 21 𝐽 ∈ (TopOn‘ℂ)
1514toponunii 20495 . . . . . . . . . . . . . . . . . . . 20 ℂ = 𝐽
1615cldss 20591 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ (Clsd‘𝐽) → 𝑋 ⊆ ℂ)
1716adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ ℂ)
1817adantr 480 . . . . . . . . . . . . . . . . 17 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → 𝑋 ⊆ ℂ)
19 simprr 792 . . . . . . . . . . . . . . . . 17 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (𝐹𝑢) ∈ 𝑋)
2018, 19sseldd 3569 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (𝐹𝑢) ∈ ℂ)
2120abscld 13972 . . . . . . . . . . . . . . 15 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(𝐹𝑢)) ∈ ℝ)
22 simplrl 796 . . . . . . . . . . . . . . 15 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → 𝑅 ∈ ℝ)
23 simprl 790 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → 𝑢 ∈ (ℝ × ℝ))
24 f1ocnvfv1 6410 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(ℝ × ℝ)–1-1-onto→ℂ ∧ 𝑢 ∈ (ℝ × ℝ)) → (𝐹‘(𝐹𝑢)) = 𝑢)
254, 23, 24sylancr 694 . . . . . . . . . . . . . . . . . . . 20 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (𝐹‘(𝐹𝑢)) = 𝑢)
26 fveq2 6088 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝐹𝑢) → (ℜ‘𝑧) = (ℜ‘(𝐹𝑢)))
27 fveq2 6088 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝐹𝑢) → (ℑ‘𝑧) = (ℑ‘(𝐹𝑢)))
2826, 27opeq12d 4343 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (𝐹𝑢) → ⟨(ℜ‘𝑧), (ℑ‘𝑧)⟩ = ⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩)
293cnrecnv 13702 . . . . . . . . . . . . . . . . . . . . . 22 𝐹 = (𝑧 ∈ ℂ ↦ ⟨(ℜ‘𝑧), (ℑ‘𝑧)⟩)
30 opex 4853 . . . . . . . . . . . . . . . . . . . . . 22 ⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩ ∈ V
3128, 29, 30fvmpt 6176 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑢) ∈ ℂ → (𝐹‘(𝐹𝑢)) = ⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩)
3220, 31syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (𝐹‘(𝐹𝑢)) = ⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩)
3325, 32eqtr3d 2646 . . . . . . . . . . . . . . . . . . 19 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → 𝑢 = ⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩)
3433fveq2d 6092 . . . . . . . . . . . . . . . . . 18 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (1st𝑢) = (1st ‘⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩))
35 fvex 6098 . . . . . . . . . . . . . . . . . . 19 (ℜ‘(𝐹𝑢)) ∈ V
36 fvex 6098 . . . . . . . . . . . . . . . . . . 19 (ℑ‘(𝐹𝑢)) ∈ V
3735, 36op1st 7045 . . . . . . . . . . . . . . . . . 18 (1st ‘⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩) = (ℜ‘(𝐹𝑢))
3834, 37syl6eq 2660 . . . . . . . . . . . . . . . . 17 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (1st𝑢) = (ℜ‘(𝐹𝑢)))
3938fveq2d 6092 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(1st𝑢)) = (abs‘(ℜ‘(𝐹𝑢))))
40 absrele 13845 . . . . . . . . . . . . . . . . 17 ((𝐹𝑢) ∈ ℂ → (abs‘(ℜ‘(𝐹𝑢))) ≤ (abs‘(𝐹𝑢)))
4120, 40syl 17 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(ℜ‘(𝐹𝑢))) ≤ (abs‘(𝐹𝑢)))
4239, 41eqbrtrd 4600 . . . . . . . . . . . . . . 15 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(1st𝑢)) ≤ (abs‘(𝐹𝑢)))
43 simplrr 797 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)
44 fveq2 6088 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝐹𝑢) → (abs‘𝑧) = (abs‘(𝐹𝑢)))
4544breq1d 4588 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝐹𝑢) → ((abs‘𝑧) ≤ 𝑅 ↔ (abs‘(𝐹𝑢)) ≤ 𝑅))
4645rspcv 3278 . . . . . . . . . . . . . . . 16 ((𝐹𝑢) ∈ 𝑋 → (∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅 → (abs‘(𝐹𝑢)) ≤ 𝑅))
4719, 43, 46sylc 63 . . . . . . . . . . . . . . 15 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(𝐹𝑢)) ≤ 𝑅)
4813, 21, 22, 42, 47letrd 10046 . . . . . . . . . . . . . 14 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(1st𝑢)) ≤ 𝑅)
4911, 22absled 13966 . . . . . . . . . . . . . 14 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → ((abs‘(1st𝑢)) ≤ 𝑅 ↔ (-𝑅 ≤ (1st𝑢) ∧ (1st𝑢) ≤ 𝑅)))
5048, 49mpbid 221 . . . . . . . . . . . . 13 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (-𝑅 ≤ (1st𝑢) ∧ (1st𝑢) ≤ 𝑅))
5150simpld 474 . . . . . . . . . . . 12 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → -𝑅 ≤ (1st𝑢))
5250simprd 478 . . . . . . . . . . . 12 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (1st𝑢) ≤ 𝑅)
53 renegcl 10196 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ → -𝑅 ∈ ℝ)
5422, 53syl 17 . . . . . . . . . . . . 13 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → -𝑅 ∈ ℝ)
55 elicc2 12068 . . . . . . . . . . . . 13 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((1st𝑢) ∈ (-𝑅[,]𝑅) ↔ ((1st𝑢) ∈ ℝ ∧ -𝑅 ≤ (1st𝑢) ∧ (1st𝑢) ≤ 𝑅)))
5654, 22, 55syl2anc 691 . . . . . . . . . . . 12 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → ((1st𝑢) ∈ (-𝑅[,]𝑅) ↔ ((1st𝑢) ∈ ℝ ∧ -𝑅 ≤ (1st𝑢) ∧ (1st𝑢) ≤ 𝑅)))
5711, 51, 52, 56mpbir3and 1238 . . . . . . . . . . 11 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (1st𝑢) ∈ (-𝑅[,]𝑅))
58 xp2nd 7068 . . . . . . . . . . . . 13 (𝑢 ∈ (ℝ × ℝ) → (2nd𝑢) ∈ ℝ)
5958ad2antrl 760 . . . . . . . . . . . 12 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (2nd𝑢) ∈ ℝ)
6059recnd 9925 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (2nd𝑢) ∈ ℂ)
6160abscld 13972 . . . . . . . . . . . . . . 15 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(2nd𝑢)) ∈ ℝ)
6233fveq2d 6092 . . . . . . . . . . . . . . . . . 18 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (2nd𝑢) = (2nd ‘⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩))
6335, 36op2nd 7046 . . . . . . . . . . . . . . . . . 18 (2nd ‘⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩) = (ℑ‘(𝐹𝑢))
6462, 63syl6eq 2660 . . . . . . . . . . . . . . . . 17 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (2nd𝑢) = (ℑ‘(𝐹𝑢)))
6564fveq2d 6092 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(2nd𝑢)) = (abs‘(ℑ‘(𝐹𝑢))))
66 absimle 13846 . . . . . . . . . . . . . . . . 17 ((𝐹𝑢) ∈ ℂ → (abs‘(ℑ‘(𝐹𝑢))) ≤ (abs‘(𝐹𝑢)))
6720, 66syl 17 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(ℑ‘(𝐹𝑢))) ≤ (abs‘(𝐹𝑢)))
6865, 67eqbrtrd 4600 . . . . . . . . . . . . . . 15 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(2nd𝑢)) ≤ (abs‘(𝐹𝑢)))
6961, 21, 22, 68, 47letrd 10046 . . . . . . . . . . . . . 14 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(2nd𝑢)) ≤ 𝑅)
7059, 22absled 13966 . . . . . . . . . . . . . 14 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → ((abs‘(2nd𝑢)) ≤ 𝑅 ↔ (-𝑅 ≤ (2nd𝑢) ∧ (2nd𝑢) ≤ 𝑅)))
7169, 70mpbid 221 . . . . . . . . . . . . 13 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (-𝑅 ≤ (2nd𝑢) ∧ (2nd𝑢) ≤ 𝑅))
7271simpld 474 . . . . . . . . . . . 12 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → -𝑅 ≤ (2nd𝑢))
7371simprd 478 . . . . . . . . . . . 12 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (2nd𝑢) ≤ 𝑅)
74 elicc2 12068 . . . . . . . . . . . . 13 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((2nd𝑢) ∈ (-𝑅[,]𝑅) ↔ ((2nd𝑢) ∈ ℝ ∧ -𝑅 ≤ (2nd𝑢) ∧ (2nd𝑢) ≤ 𝑅)))
7554, 22, 74syl2anc 691 . . . . . . . . . . . 12 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → ((2nd𝑢) ∈ (-𝑅[,]𝑅) ↔ ((2nd𝑢) ∈ ℝ ∧ -𝑅 ≤ (2nd𝑢) ∧ (2nd𝑢) ≤ 𝑅)))
7659, 72, 73, 75mpbir3and 1238 . . . . . . . . . . 11 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (2nd𝑢) ∈ (-𝑅[,]𝑅))
7757, 76opelxpd 5063 . . . . . . . . . 10 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → ⟨(1st𝑢), (2nd𝑢)⟩ ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))
789, 77eqeltrd 2688 . . . . . . . . 9 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))
7978ex 449 . . . . . . . 8 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))
807, 79syl5bi 231 . . . . . . 7 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → (𝑢 ∈ (𝐹𝑋) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))
8180ssrdv 3574 . . . . . 6 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → (𝐹𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))
82 f1ofun 6037 . . . . . . . 8 (𝐹:(ℝ × ℝ)–1-1-onto→ℂ → Fun 𝐹)
834, 82ax-mp 5 . . . . . . 7 Fun 𝐹
84 f1ofo 6042 . . . . . . . . 9 (𝐹:(ℝ × ℝ)–1-1-onto→ℂ → 𝐹:(ℝ × ℝ)–onto→ℂ)
85 forn 6016 . . . . . . . . 9 (𝐹:(ℝ × ℝ)–onto→ℂ → ran 𝐹 = ℂ)
864, 84, 85mp2b 10 . . . . . . . 8 ran 𝐹 = ℂ
8717, 86syl6sseqr 3615 . . . . . . 7 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ ran 𝐹)
88 funimass1 5871 . . . . . . 7 ((Fun 𝐹𝑋 ⊆ ran 𝐹) → ((𝐹𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))))
8983, 87, 88sylancr 694 . . . . . 6 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐹𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))))
9081, 89mpd 15 . . . . 5 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))
91 cnheibor.5 . . . . 5 𝑌 = (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))
9290, 91syl6sseqr 3615 . . . 4 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋𝑌)
93 eqid 2610 . . . . . . . 8 (topGen‘ran (,)) = (topGen‘ran (,))
943, 93, 1cnrehmeo 22508 . . . . . . 7 𝐹 ∈ (((topGen‘ran (,)) ×t (topGen‘ran (,)))Homeo𝐽)
95 imaexg 6973 . . . . . . 7 (𝐹 ∈ (((topGen‘ran (,)) ×t (topGen‘ran (,)))Homeo𝐽) → (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ V)
9694, 95ax-mp 5 . . . . . 6 (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ V
9791, 96eqeltri 2684 . . . . 5 𝑌 ∈ V
9897a1i 11 . . . 4 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑌 ∈ V)
99 restabs 20727 . . . 4 ((𝐽 ∈ Top ∧ 𝑋𝑌𝑌 ∈ V) → ((𝐽t 𝑌) ↾t 𝑋) = (𝐽t 𝑋))
1002, 92, 98, 99mp3an2i 1421 . . 3 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽t 𝑌) ↾t 𝑋) = (𝐽t 𝑋))
101 cnheibor.3 . . 3 𝑇 = (𝐽t 𝑋)
102100, 101syl6eqr 2662 . 2 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽t 𝑌) ↾t 𝑋) = 𝑇)
10391oveq2i 6538 . . . . 5 (𝐽t 𝑌) = (𝐽t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))
104 ishmeo 21320 . . . . . . . 8 (𝐹 ∈ (((topGen‘ran (,)) ×t (topGen‘ran (,)))Homeo𝐽) ↔ (𝐹 ∈ (((topGen‘ran (,)) ×t (topGen‘ran (,))) Cn 𝐽) ∧ 𝐹 ∈ (𝐽 Cn ((topGen‘ran (,)) ×t (topGen‘ran (,))))))
10594, 104mpbi 219 . . . . . . 7 (𝐹 ∈ (((topGen‘ran (,)) ×t (topGen‘ran (,))) Cn 𝐽) ∧ 𝐹 ∈ (𝐽 Cn ((topGen‘ran (,)) ×t (topGen‘ran (,)))))
106105simpli 473 . . . . . 6 𝐹 ∈ (((topGen‘ran (,)) ×t (topGen‘ran (,))) Cn 𝐽)
107 iccssre 12085 . . . . . . . . . . 11 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ)
10853, 107mpancom 700 . . . . . . . . . 10 (𝑅 ∈ ℝ → (-𝑅[,]𝑅) ⊆ ℝ)
1091, 93rerest 22363 . . . . . . . . . 10 ((-𝑅[,]𝑅) ⊆ ℝ → (𝐽t (-𝑅[,]𝑅)) = ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)))
110108, 109syl 17 . . . . . . . . 9 (𝑅 ∈ ℝ → (𝐽t (-𝑅[,]𝑅)) = ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)))
111110, 110oveq12d 6545 . . . . . . . 8 (𝑅 ∈ ℝ → ((𝐽t (-𝑅[,]𝑅)) ×t (𝐽t (-𝑅[,]𝑅))) = (((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ×t ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅))))
112 retop 22323 . . . . . . . . 9 (topGen‘ran (,)) ∈ Top
113 ovex 6555 . . . . . . . . 9 (-𝑅[,]𝑅) ∈ V
114 txrest 21192 . . . . . . . . 9 ((((topGen‘ran (,)) ∈ Top ∧ (topGen‘ran (,)) ∈ Top) ∧ ((-𝑅[,]𝑅) ∈ V ∧ (-𝑅[,]𝑅) ∈ V)) → (((topGen‘ran (,)) ×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) = (((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ×t ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅))))
115112, 112, 113, 113, 114mp4an 705 . . . . . . . 8 (((topGen‘ran (,)) ×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) = (((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ×t ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)))
116111, 115syl6eqr 2662 . . . . . . 7 (𝑅 ∈ ℝ → ((𝐽t (-𝑅[,]𝑅)) ×t (𝐽t (-𝑅[,]𝑅))) = (((topGen‘ran (,)) ×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))
117 eqid 2610 . . . . . . . . . . 11 ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) = ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅))
11893, 117icccmp 22384 . . . . . . . . . 10 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ∈ Comp)
11953, 118mpancom 700 . . . . . . . . 9 (𝑅 ∈ ℝ → ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ∈ Comp)
120110, 119eqeltrd 2688 . . . . . . . 8 (𝑅 ∈ ℝ → (𝐽t (-𝑅[,]𝑅)) ∈ Comp)
121 txcmp 21204 . . . . . . . 8 (((𝐽t (-𝑅[,]𝑅)) ∈ Comp ∧ (𝐽t (-𝑅[,]𝑅)) ∈ Comp) → ((𝐽t (-𝑅[,]𝑅)) ×t (𝐽t (-𝑅[,]𝑅))) ∈ Comp)
122120, 120, 121syl2anc 691 . . . . . . 7 (𝑅 ∈ ℝ → ((𝐽t (-𝑅[,]𝑅)) ×t (𝐽t (-𝑅[,]𝑅))) ∈ Comp)
123116, 122eqeltrrd 2689 . . . . . 6 (𝑅 ∈ ℝ → (((topGen‘ran (,)) ×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ Comp)
124 imacmp 20958 . . . . . 6 ((𝐹 ∈ (((topGen‘ran (,)) ×t (topGen‘ran (,))) Cn 𝐽) ∧ (((topGen‘ran (,)) ×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ Comp) → (𝐽t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) ∈ Comp)
125106, 123, 124sylancr 694 . . . . 5 (𝑅 ∈ ℝ → (𝐽t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) ∈ Comp)
126103, 125syl5eqel 2692 . . . 4 (𝑅 ∈ ℝ → (𝐽t 𝑌) ∈ Comp)
127126ad2antrl 760 . . 3 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → (𝐽t 𝑌) ∈ Comp)
128 imassrn 5383 . . . . . 6 (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ⊆ ran 𝐹
12991, 128eqsstri 3598 . . . . 5 𝑌 ⊆ ran 𝐹
130 f1of 6035 . . . . . 6 (𝐹:(ℝ × ℝ)–1-1-onto→ℂ → 𝐹:(ℝ × ℝ)⟶ℂ)
131 frn 5952 . . . . . 6 (𝐹:(ℝ × ℝ)⟶ℂ → ran 𝐹 ⊆ ℂ)
1324, 130, 131mp2b 10 . . . . 5 ran 𝐹 ⊆ ℂ
133129, 132sstri 3577 . . . 4 𝑌 ⊆ ℂ
134 simpl 472 . . . 4 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ∈ (Clsd‘𝐽))
13515restcldi 20735 . . . 4 ((𝑌 ⊆ ℂ ∧ 𝑋 ∈ (Clsd‘𝐽) ∧ 𝑋𝑌) → 𝑋 ∈ (Clsd‘(𝐽t 𝑌)))
136133, 134, 92, 135mp3an2i 1421 . . 3 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ∈ (Clsd‘(𝐽t 𝑌)))
137 cmpcld 20963 . . 3 (((𝐽t 𝑌) ∈ Comp ∧ 𝑋 ∈ (Clsd‘(𝐽t 𝑌))) → ((𝐽t 𝑌) ↾t 𝑋) ∈ Comp)
138127, 136, 137syl2anc 691 . 2 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽t 𝑌) ↾t 𝑋) ∈ Comp)
139102, 138eqeltrrd 2689 1 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑇 ∈ Comp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wcel 1977  wral 2896  Vcvv 3173  wss 3540  cop 4131   class class class wbr 4578   × cxp 5026  ccnv 5027  ran crn 5029  cima 5031  Fun wfun 5784   Fn wfn 5785  wf 5786  ontowfo 5788  1-1-ontowf1o 5789  cfv 5790  (class class class)co 6527  cmpt2 6529  1st c1st 7035  2nd c2nd 7036  cc 9791  cr 9792  ici 9795   + caddc 9796   · cmul 9798  cle 9932  -cneg 10119  (,)cioo 12005  [,]cicc 12008  cre 13634  cim 13635  abscabs 13771  t crest 15853  TopOpenctopn 15854  topGenctg 15870  fldccnfld 19516  Topctop 20465  Clsdccld 20578   Cn ccn 20786  Compccmp 20947   ×t ctx 21121  Homeochmeo 21314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4694  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871  ax-addf 9872  ax-mulf 9873
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4368  df-int 4406  df-iun 4452  df-iin 4453  df-br 4579  df-opab 4639  df-mpt 4640  df-tr 4676  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-om 6936  df-1st 7037  df-2nd 7038  df-supp 7161  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-map 7724  df-ixp 7773  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fsupp 8137  df-fi 8178  df-sup 8209  df-inf 8210  df-oi 8276  df-card 8626  df-cda 8851  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-4 10931  df-5 10932  df-6 10933  df-7 10934  df-8 10935  df-9 10936  df-n0 11143  df-z 11214  df-dec 11329  df-uz 11523  df-q 11624  df-rp 11668  df-xneg 11781  df-xadd 11782  df-xmul 11783  df-ioo 12009  df-icc 12012  df-fz 12156  df-fzo 12293  df-seq 12622  df-exp 12681  df-hash 12938  df-cj 13636  df-re 13637  df-im 13638  df-sqrt 13772  df-abs 13773  df-struct 15646  df-ndx 15647  df-slot 15648  df-base 15649  df-sets 15650  df-ress 15651  df-plusg 15730  df-mulr 15731  df-starv 15732  df-sca 15733  df-vsca 15734  df-ip 15735  df-tset 15736  df-ple 15737  df-ds 15740  df-unif 15741  df-hom 15742  df-cco 15743  df-rest 15855  df-topn 15856  df-0g 15874  df-gsum 15875  df-topgen 15876  df-pt 15877  df-prds 15880  df-xrs 15934  df-qtop 15939  df-imas 15940  df-xps 15942  df-mre 16018  df-mrc 16019  df-acs 16021  df-mgm 17014  df-sgrp 17056  df-mnd 17067  df-submnd 17108  df-mulg 17313  df-cntz 17522  df-cmn 17967  df-psmet 19508  df-xmet 19509  df-met 19510  df-bl 19511  df-mopn 19512  df-cnfld 19517  df-top 20469  df-bases 20470  df-topon 20471  df-topsp 20472  df-cld 20581  df-cn 20789  df-cnp 20790  df-cmp 20948  df-tx 21123  df-hmeo 21316  df-xms 21883  df-ms 21884  df-tms 21885  df-cncf 22437
This theorem is referenced by:  cnheibor  22510
  Copyright terms: Public domain W3C validator