This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iihalf1cnOLD

Description: Obsolete version of iihalf1cn as of 9-Apr-2025. (Contributed by Mario Carneiro, 6-Jun-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis iihalf1cnOLD.1 ⊢ 𝐽 = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) )
Assertion iihalf1cnOLD ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑥 ) ) ∈ ( 𝐽 Cn II )

Proof

Step Hyp Ref Expression
1 iihalf1cnOLD.1 ⊢ 𝐽 = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) )
2 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
3 dfii2 ⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
4 0re ⊢ 0 ∈ ℝ
5 halfre ⊢ ( 1 / 2 ) ∈ ℝ
6 iccssre ⊢ ( ( 0 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ )
7 4 5 6 mp2an ⊢ ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ
8 7 a1i ⊢ ( ⊤ → ( 0 [,] ( 1 / 2 ) ) ⊆ ℝ )
9 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
10 9 a1i ⊢ ( ⊤ → ( 0 [,] 1 ) ⊆ ℝ )
11 iihalf1 ⊢ ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) → ( 2 · 𝑥 ) ∈ ( 0 [,] 1 ) )
12 11 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ) → ( 2 · 𝑥 ) ∈ ( 0 [,] 1 ) )
13 2 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
14 13 a1i ⊢ ( ⊤ → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
15 2cnd ⊢ ( ⊤ → 2 ∈ ℂ )
16 14 14 15 cnmptc ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ 2 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
17 14 cnmptid ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
18 2 mulcn ⊢ · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
19 18 a1i ⊢ ( ⊤ → · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
20 14 16 17 19 cnmpt12f ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( 2 · 𝑥 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
21 2 1 3 8 10 12 20 cnmptre ⊢ ( ⊤ → ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑥 ) ) ∈ ( 𝐽 Cn II ) )
22 21 mptru ⊢ ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ↦ ( 2 · 𝑥 ) ) ∈ ( 𝐽 Cn II )