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

Theorem cnheiborlem 24898
Description: Lemma for cnheibor 24899. (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 24718 . . . 4 𝐽 ∈ Top
3 cnheibor.4 . . . . . . . . . 10 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))
43cnref1o 13005 . . . . . . . . 9 𝐹:(ℝ × ℝ)–1-1-onto→ℂ
5 f1ofn 6843 . . . . . . . . 9 (𝐹:(ℝ × ℝ)–1-1-onto→ℂ → 𝐹 Fn (ℝ × ℝ))
6 elpreima 7070 . . . . . . . . 9 (𝐹 Fn (ℝ × ℝ) → (𝑢 ∈ (𝐹𝑋) ↔ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)))
74, 5, 6mp2b 10 . . . . . . . 8 (𝑢 ∈ (𝐹𝑋) ↔ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋))
8 1st2nd2 8036 . . . . . . . . . . 11 (𝑢 ∈ (ℝ × ℝ) → 𝑢 = ⟨(1st𝑢), (2nd𝑢)⟩)
98ad2antrl 726 . . . . . . . . . 10 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → 𝑢 = ⟨(1st𝑢), (2nd𝑢)⟩)
10 xp1st 8029 . . . . . . . . . . . . 13 (𝑢 ∈ (ℝ × ℝ) → (1st𝑢) ∈ ℝ)
1110ad2antrl 726 . . . . . . . . . . . 12 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (1st𝑢) ∈ ℝ)
1211recnd 11278 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (1st𝑢) ∈ ℂ)
1312abscld 15421 . . . . . . . . . . . . . . 15 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(1st𝑢)) ∈ ℝ)
141cnfldtopon 24717 . . . . . . . . . . . . . . . . . . . . 21 𝐽 ∈ (TopOn‘ℂ)
1514toponunii 22836 . . . . . . . . . . . . . . . . . . . 20 ℂ = 𝐽
1615cldss 22951 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ (Clsd‘𝐽) → 𝑋 ⊆ ℂ)
1716adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ ℂ)
1817adantr 479 . . . . . . . . . . . . . . . . 17 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → 𝑋 ⊆ ℂ)
19 simprr 771 . . . . . . . . . . . . . . . . 17 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (𝐹𝑢) ∈ 𝑋)
2018, 19sseldd 3981 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (𝐹𝑢) ∈ ℂ)
2120abscld 15421 . . . . . . . . . . . . . . 15 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(𝐹𝑢)) ∈ ℝ)
22 simplrl 775 . . . . . . . . . . . . . . 15 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → 𝑅 ∈ ℝ)
23 simprl 769 . . . . . . . . . . . . . . . . . . . . 21 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → 𝑢 ∈ (ℝ × ℝ))
24 f1ocnvfv1 7289 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(ℝ × ℝ)–1-1-onto→ℂ ∧ 𝑢 ∈ (ℝ × ℝ)) → (𝐹‘(𝐹𝑢)) = 𝑢)
254, 23, 24sylancr 585 . . . . . . . . . . . . . . . . . . . 20 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (𝐹‘(𝐹𝑢)) = 𝑢)
26 fveq2 6900 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝐹𝑢) → (ℜ‘𝑧) = (ℜ‘(𝐹𝑢)))
27 fveq2 6900 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝐹𝑢) → (ℑ‘𝑧) = (ℑ‘(𝐹𝑢)))
2826, 27opeq12d 4884 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (𝐹𝑢) → ⟨(ℜ‘𝑧), (ℑ‘𝑧)⟩ = ⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩)
293cnrecnv 15150 . . . . . . . . . . . . . . . . . . . . . 22 𝐹 = (𝑧 ∈ ℂ ↦ ⟨(ℜ‘𝑧), (ℑ‘𝑧)⟩)
30 opex 5468 . . . . . . . . . . . . . . . . . . . . . 22 ⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩ ∈ V
3128, 29, 30fvmpt 7008 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑢) ∈ ℂ → (𝐹‘(𝐹𝑢)) = ⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩)
3220, 31syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (𝐹‘(𝐹𝑢)) = ⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩)
3325, 32eqtr3d 2769 . . . . . . . . . . . . . . . . . . 19 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → 𝑢 = ⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩)
3433fveq2d 6904 . . . . . . . . . . . . . . . . . 18 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (1st𝑢) = (1st ‘⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩))
35 fvex 6913 . . . . . . . . . . . . . . . . . . 19 (ℜ‘(𝐹𝑢)) ∈ V
36 fvex 6913 . . . . . . . . . . . . . . . . . . 19 (ℑ‘(𝐹𝑢)) ∈ V
3735, 36op1st 8005 . . . . . . . . . . . . . . . . . 18 (1st ‘⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩) = (ℜ‘(𝐹𝑢))
3834, 37eqtrdi 2783 . . . . . . . . . . . . . . . . 17 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (1st𝑢) = (ℜ‘(𝐹𝑢)))
3938fveq2d 6904 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(1st𝑢)) = (abs‘(ℜ‘(𝐹𝑢))))
40 absrele 15293 . . . . . . . . . . . . . . . . 17 ((𝐹𝑢) ∈ ℂ → (abs‘(ℜ‘(𝐹𝑢))) ≤ (abs‘(𝐹𝑢)))
4120, 40syl 17 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(ℜ‘(𝐹𝑢))) ≤ (abs‘(𝐹𝑢)))
4239, 41eqbrtrd 5172 . . . . . . . . . . . . . . 15 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(1st𝑢)) ≤ (abs‘(𝐹𝑢)))
43 fveq2 6900 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝐹𝑢) → (abs‘𝑧) = (abs‘(𝐹𝑢)))
4443breq1d 5160 . . . . . . . . . . . . . . . 16 (𝑧 = (𝐹𝑢) → ((abs‘𝑧) ≤ 𝑅 ↔ (abs‘(𝐹𝑢)) ≤ 𝑅))
45 simplrr 776 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)
4644, 45, 19rspcdva 3610 . . . . . . . . . . . . . . 15 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(𝐹𝑢)) ≤ 𝑅)
4713, 21, 22, 42, 46letrd 11407 . . . . . . . . . . . . . 14 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(1st𝑢)) ≤ 𝑅)
4811, 22absled 15415 . . . . . . . . . . . . . 14 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → ((abs‘(1st𝑢)) ≤ 𝑅 ↔ (-𝑅 ≤ (1st𝑢) ∧ (1st𝑢) ≤ 𝑅)))
4947, 48mpbid 231 . . . . . . . . . . . . 13 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (-𝑅 ≤ (1st𝑢) ∧ (1st𝑢) ≤ 𝑅))
5049simpld 493 . . . . . . . . . . . 12 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → -𝑅 ≤ (1st𝑢))
5149simprd 494 . . . . . . . . . . . 12 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (1st𝑢) ≤ 𝑅)
52 renegcl 11559 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ → -𝑅 ∈ ℝ)
5322, 52syl 17 . . . . . . . . . . . . 13 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → -𝑅 ∈ ℝ)
54 elicc2 13427 . . . . . . . . . . . . 13 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((1st𝑢) ∈ (-𝑅[,]𝑅) ↔ ((1st𝑢) ∈ ℝ ∧ -𝑅 ≤ (1st𝑢) ∧ (1st𝑢) ≤ 𝑅)))
5553, 22, 54syl2anc 582 . . . . . . . . . . . 12 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → ((1st𝑢) ∈ (-𝑅[,]𝑅) ↔ ((1st𝑢) ∈ ℝ ∧ -𝑅 ≤ (1st𝑢) ∧ (1st𝑢) ≤ 𝑅)))
5611, 50, 51, 55mpbir3and 1339 . . . . . . . . . . 11 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (1st𝑢) ∈ (-𝑅[,]𝑅))
57 xp2nd 8030 . . . . . . . . . . . . 13 (𝑢 ∈ (ℝ × ℝ) → (2nd𝑢) ∈ ℝ)
5857ad2antrl 726 . . . . . . . . . . . 12 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (2nd𝑢) ∈ ℝ)
5958recnd 11278 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (2nd𝑢) ∈ ℂ)
6059abscld 15421 . . . . . . . . . . . . . . 15 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(2nd𝑢)) ∈ ℝ)
6133fveq2d 6904 . . . . . . . . . . . . . . . . . 18 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (2nd𝑢) = (2nd ‘⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩))
6235, 36op2nd 8006 . . . . . . . . . . . . . . . . . 18 (2nd ‘⟨(ℜ‘(𝐹𝑢)), (ℑ‘(𝐹𝑢))⟩) = (ℑ‘(𝐹𝑢))
6361, 62eqtrdi 2783 . . . . . . . . . . . . . . . . 17 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (2nd𝑢) = (ℑ‘(𝐹𝑢)))
6463fveq2d 6904 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(2nd𝑢)) = (abs‘(ℑ‘(𝐹𝑢))))
65 absimle 15294 . . . . . . . . . . . . . . . . 17 ((𝐹𝑢) ∈ ℂ → (abs‘(ℑ‘(𝐹𝑢))) ≤ (abs‘(𝐹𝑢)))
6620, 65syl 17 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(ℑ‘(𝐹𝑢))) ≤ (abs‘(𝐹𝑢)))
6764, 66eqbrtrd 5172 . . . . . . . . . . . . . . 15 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(2nd𝑢)) ≤ (abs‘(𝐹𝑢)))
6860, 21, 22, 67, 46letrd 11407 . . . . . . . . . . . . . 14 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (abs‘(2nd𝑢)) ≤ 𝑅)
6958, 22absled 15415 . . . . . . . . . . . . . 14 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → ((abs‘(2nd𝑢)) ≤ 𝑅 ↔ (-𝑅 ≤ (2nd𝑢) ∧ (2nd𝑢) ≤ 𝑅)))
7068, 69mpbid 231 . . . . . . . . . . . . 13 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (-𝑅 ≤ (2nd𝑢) ∧ (2nd𝑢) ≤ 𝑅))
7170simpld 493 . . . . . . . . . . . 12 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → -𝑅 ≤ (2nd𝑢))
7270simprd 494 . . . . . . . . . . . 12 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (2nd𝑢) ≤ 𝑅)
73 elicc2 13427 . . . . . . . . . . . . 13 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((2nd𝑢) ∈ (-𝑅[,]𝑅) ↔ ((2nd𝑢) ∈ ℝ ∧ -𝑅 ≤ (2nd𝑢) ∧ (2nd𝑢) ≤ 𝑅)))
7453, 22, 73syl2anc 582 . . . . . . . . . . . 12 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → ((2nd𝑢) ∈ (-𝑅[,]𝑅) ↔ ((2nd𝑢) ∈ ℝ ∧ -𝑅 ≤ (2nd𝑢) ∧ (2nd𝑢) ≤ 𝑅)))
7558, 71, 72, 74mpbir3and 1339 . . . . . . . . . . 11 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → (2nd𝑢) ∈ (-𝑅[,]𝑅))
7656, 75opelxpd 5719 . . . . . . . . . 10 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → ⟨(1st𝑢), (2nd𝑢)⟩ ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))
779, 76eqeltrd 2828 . . . . . . . . 9 (((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) ∧ (𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋)) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))
7877ex 411 . . . . . . . 8 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝑢 ∈ (ℝ × ℝ) ∧ (𝐹𝑢) ∈ 𝑋) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))
797, 78biimtrid 241 . . . . . . 7 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → (𝑢 ∈ (𝐹𝑋) → 𝑢 ∈ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))
8079ssrdv 3986 . . . . . 6 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → (𝐹𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))
81 f1ofun 6844 . . . . . . . 8 (𝐹:(ℝ × ℝ)–1-1-onto→ℂ → Fun 𝐹)
824, 81ax-mp 5 . . . . . . 7 Fun 𝐹
83 f1ofo 6849 . . . . . . . . 9 (𝐹:(ℝ × ℝ)–1-1-onto→ℂ → 𝐹:(ℝ × ℝ)–onto→ℂ)
84 forn 6817 . . . . . . . . 9 (𝐹:(ℝ × ℝ)–onto→ℂ → ran 𝐹 = ℂ)
854, 83, 84mp2b 10 . . . . . . . 8 ran 𝐹 = ℂ
8617, 85sseqtrrdi 4031 . . . . . . 7 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ ran 𝐹)
87 funimass1 6638 . . . . . . 7 ((Fun 𝐹𝑋 ⊆ ran 𝐹) → ((𝐹𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))))
8882, 86, 87sylancr 585 . . . . . 6 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐹𝑋) ⊆ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))))
8980, 88mpd 15 . . . . 5 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ⊆ (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))
90 cnheibor.5 . . . . 5 𝑌 = (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))
9189, 90sseqtrrdi 4031 . . . 4 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋𝑌)
92 eqid 2727 . . . . . . . 8 (topGen‘ran (,)) = (topGen‘ran (,))
933, 92, 1cnrehmeo 24896 . . . . . . 7 𝐹 ∈ (((topGen‘ran (,)) ×t (topGen‘ran (,)))Homeo𝐽)
94 imaexg 7925 . . . . . . 7 (𝐹 ∈ (((topGen‘ran (,)) ×t (topGen‘ran (,)))Homeo𝐽) → (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ V)
9593, 94ax-mp 5 . . . . . 6 (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ V
9690, 95eqeltri 2824 . . . . 5 𝑌 ∈ V
9796a1i 11 . . . 4 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑌 ∈ V)
98 restabs 23087 . . . 4 ((𝐽 ∈ Top ∧ 𝑋𝑌𝑌 ∈ V) → ((𝐽t 𝑌) ↾t 𝑋) = (𝐽t 𝑋))
992, 91, 97, 98mp3an2i 1462 . . 3 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽t 𝑌) ↾t 𝑋) = (𝐽t 𝑋))
100 cnheibor.3 . . 3 𝑇 = (𝐽t 𝑋)
10199, 100eqtr4di 2785 . 2 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽t 𝑌) ↾t 𝑋) = 𝑇)
10290oveq2i 7435 . . . . 5 (𝐽t 𝑌) = (𝐽t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))
103 ishmeo 23681 . . . . . . . 8 (𝐹 ∈ (((topGen‘ran (,)) ×t (topGen‘ran (,)))Homeo𝐽) ↔ (𝐹 ∈ (((topGen‘ran (,)) ×t (topGen‘ran (,))) Cn 𝐽) ∧ 𝐹 ∈ (𝐽 Cn ((topGen‘ran (,)) ×t (topGen‘ran (,))))))
10493, 103mpbi 229 . . . . . . 7 (𝐹 ∈ (((topGen‘ran (,)) ×t (topGen‘ran (,))) Cn 𝐽) ∧ 𝐹 ∈ (𝐽 Cn ((topGen‘ran (,)) ×t (topGen‘ran (,)))))
105104simpli 482 . . . . . 6 𝐹 ∈ (((topGen‘ran (,)) ×t (topGen‘ran (,))) Cn 𝐽)
106 iccssre 13444 . . . . . . . . . . 11 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ)
10752, 106mpancom 686 . . . . . . . . . 10 (𝑅 ∈ ℝ → (-𝑅[,]𝑅) ⊆ ℝ)
1081, 92rerest 24738 . . . . . . . . . 10 ((-𝑅[,]𝑅) ⊆ ℝ → (𝐽t (-𝑅[,]𝑅)) = ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)))
109107, 108syl 17 . . . . . . . . 9 (𝑅 ∈ ℝ → (𝐽t (-𝑅[,]𝑅)) = ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)))
110109, 109oveq12d 7442 . . . . . . . 8 (𝑅 ∈ ℝ → ((𝐽t (-𝑅[,]𝑅)) ×t (𝐽t (-𝑅[,]𝑅))) = (((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ×t ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅))))
111 retop 24696 . . . . . . . . 9 (topGen‘ran (,)) ∈ Top
112 ovex 7457 . . . . . . . . 9 (-𝑅[,]𝑅) ∈ V
113 txrest 23553 . . . . . . . . 9 ((((topGen‘ran (,)) ∈ Top ∧ (topGen‘ran (,)) ∈ Top) ∧ ((-𝑅[,]𝑅) ∈ V ∧ (-𝑅[,]𝑅) ∈ V)) → (((topGen‘ran (,)) ×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) = (((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ×t ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅))))
114111, 111, 112, 112, 113mp4an 691 . . . . . . . 8 (((topGen‘ran (,)) ×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) = (((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ×t ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)))
115110, 114eqtr4di 2785 . . . . . . 7 (𝑅 ∈ ℝ → ((𝐽t (-𝑅[,]𝑅)) ×t (𝐽t (-𝑅[,]𝑅))) = (((topGen‘ran (,)) ×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))))
116 eqid 2727 . . . . . . . . . . 11 ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) = ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅))
11792, 116icccmp 24759 . . . . . . . . . 10 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ∈ Comp)
11852, 117mpancom 686 . . . . . . . . 9 (𝑅 ∈ ℝ → ((topGen‘ran (,)) ↾t (-𝑅[,]𝑅)) ∈ Comp)
119109, 118eqeltrd 2828 . . . . . . . 8 (𝑅 ∈ ℝ → (𝐽t (-𝑅[,]𝑅)) ∈ Comp)
120 txcmp 23565 . . . . . . . 8 (((𝐽t (-𝑅[,]𝑅)) ∈ Comp ∧ (𝐽t (-𝑅[,]𝑅)) ∈ Comp) → ((𝐽t (-𝑅[,]𝑅)) ×t (𝐽t (-𝑅[,]𝑅))) ∈ Comp)
121119, 119, 120syl2anc 582 . . . . . . 7 (𝑅 ∈ ℝ → ((𝐽t (-𝑅[,]𝑅)) ×t (𝐽t (-𝑅[,]𝑅))) ∈ Comp)
122115, 121eqeltrrd 2829 . . . . . 6 (𝑅 ∈ ℝ → (((topGen‘ran (,)) ×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ Comp)
123 imacmp 23319 . . . . . 6 ((𝐹 ∈ (((topGen‘ran (,)) ×t (topGen‘ran (,))) Cn 𝐽) ∧ (((topGen‘ran (,)) ×t (topGen‘ran (,))) ↾t ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ∈ Comp) → (𝐽t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) ∈ Comp)
124105, 122, 123sylancr 585 . . . . 5 (𝑅 ∈ ℝ → (𝐽t (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))) ∈ Comp)
125102, 124eqeltrid 2832 . . . 4 (𝑅 ∈ ℝ → (𝐽t 𝑌) ∈ Comp)
126125ad2antrl 726 . . 3 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → (𝐽t 𝑌) ∈ Comp)
127 imassrn 6077 . . . . . 6 (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ⊆ ran 𝐹
12890, 127eqsstri 4014 . . . . 5 𝑌 ⊆ ran 𝐹
129 f1of 6842 . . . . . 6 (𝐹:(ℝ × ℝ)–1-1-onto→ℂ → 𝐹:(ℝ × ℝ)⟶ℂ)
130 frn 6732 . . . . . 6 (𝐹:(ℝ × ℝ)⟶ℂ → ran 𝐹 ⊆ ℂ)
1314, 129, 130mp2b 10 . . . . 5 ran 𝐹 ⊆ ℂ
132128, 131sstri 3989 . . . 4 𝑌 ⊆ ℂ
133 simpl 481 . . . 4 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ∈ (Clsd‘𝐽))
13415restcldi 23095 . . . 4 ((𝑌 ⊆ ℂ ∧ 𝑋 ∈ (Clsd‘𝐽) ∧ 𝑋𝑌) → 𝑋 ∈ (Clsd‘(𝐽t 𝑌)))
135132, 133, 91, 134mp3an2i 1462 . . 3 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑋 ∈ (Clsd‘(𝐽t 𝑌)))
136 cmpcld 23324 . . 3 (((𝐽t 𝑌) ∈ Comp ∧ 𝑋 ∈ (Clsd‘(𝐽t 𝑌))) → ((𝐽t 𝑌) ↾t 𝑋) ∈ Comp)
137126, 135, 136syl2anc 582 . 2 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → ((𝐽t 𝑌) ↾t 𝑋) ∈ Comp)
138101, 137eqeltrrd 2829 1 ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑇 ∈ Comp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3057  Vcvv 3471  wss 3947  cop 4636   class class class wbr 5150   × cxp 5678  ccnv 5679  ran crn 5681  cima 5683  Fun wfun 6545   Fn wfn 6546  wf 6547  ontowfo 6549  1-1-ontowf1o 6550  cfv 6551  (class class class)co 7424  cmpo 7426  1st c1st 7995  2nd c2nd 7996  cc 11142  cr 11143  ici 11146   + caddc 11147   · cmul 11149  cle 11285  -cneg 11481  (,)cioo 13362  [,]cicc 13365  cre 15082  cim 15083  abscabs 15219  t crest 17407  TopOpenctopn 17408  topGenctg 17424  fldccnfld 21284  Topctop 22813  Clsdccld 22938   Cn ccn 23146  Compccmp 23308   ×t ctx 23482  Homeochmeo 23675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2698  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7744  ax-cnex 11200  ax-resscn 11201  ax-1cn 11202  ax-icn 11203  ax-addcl 11204  ax-addrcl 11205  ax-mulcl 11206  ax-mulrcl 11207  ax-mulcom 11208  ax-addass 11209  ax-mulass 11210  ax-distr 11211  ax-i2m1 11212  ax-1ne0 11213  ax-1rid 11214  ax-rnegex 11215  ax-rrecex 11216  ax-cnre 11217  ax-pre-lttri 11218  ax-pre-lttrn 11219  ax-pre-ltadd 11220  ax-pre-mulgt0 11221  ax-pre-sup 11222  ax-addf 11223
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4911  df-int 4952  df-iun 5000  df-iin 5001  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5635  df-se 5636  df-we 5637  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-pred 6308  df-ord 6375  df-on 6376  df-lim 6377  df-suc 6378  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-isom 6560  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-of 7689  df-om 7875  df-1st 7997  df-2nd 7998  df-supp 8170  df-frecs 8291  df-wrecs 8322  df-recs 8396  df-rdg 8435  df-1o 8491  df-2o 8492  df-er 8729  df-map 8851  df-ixp 8921  df-en 8969  df-dom 8970  df-sdom 8971  df-fin 8972  df-fsupp 9392  df-fi 9440  df-sup 9471  df-inf 9472  df-oi 9539  df-card 9968  df-pnf 11286  df-mnf 11287  df-xr 11288  df-ltxr 11289  df-le 11290  df-sub 11482  df-neg 11483  df-div 11908  df-nn 12249  df-2 12311  df-3 12312  df-4 12313  df-5 12314  df-6 12315  df-7 12316  df-8 12317  df-9 12318  df-n0 12509  df-z 12595  df-dec 12714  df-uz 12859  df-q 12969  df-rp 13013  df-xneg 13130  df-xadd 13131  df-xmul 13132  df-ioo 13366  df-icc 13369  df-fz 13523  df-fzo 13666  df-seq 14005  df-exp 14065  df-hash 14328  df-cj 15084  df-re 15085  df-im 15086  df-sqrt 15220  df-abs 15221  df-struct 17121  df-sets 17138  df-slot 17156  df-ndx 17168  df-base 17186  df-ress 17215  df-plusg 17251  df-mulr 17252  df-starv 17253  df-sca 17254  df-vsca 17255  df-ip 17256  df-tset 17257  df-ple 17258  df-ds 17260  df-unif 17261  df-hom 17262  df-cco 17263  df-rest 17409  df-topn 17410  df-0g 17428  df-gsum 17429  df-topgen 17430  df-pt 17431  df-prds 17434  df-xrs 17489  df-qtop 17494  df-imas 17495  df-xps 17497  df-mre 17571  df-mrc 17572  df-acs 17574  df-mgm 18605  df-sgrp 18684  df-mnd 18700  df-submnd 18746  df-mulg 19029  df-cntz 19273  df-cmn 19742  df-psmet 21276  df-xmet 21277  df-met 21278  df-bl 21279  df-mopn 21280  df-cnfld 21285  df-top 22814  df-topon 22831  df-topsp 22853  df-bases 22867  df-cld 22941  df-cn 23149  df-cnp 23150  df-cmp 23309  df-tx 23484  df-hmeo 23677  df-xms 24244  df-ms 24245  df-tms 24246  df-cncf 24816
This theorem is referenced by:  cnheibor  24899
  Copyright terms: Public domain W3C validator