Metamath Proof Explorer

Theorem iimulcnOLD

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

Ref Expression
Assertion iimulcnOLD ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn II )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
2 1 dfii3 ⊢ II = ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) )
3 1 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
4 3 a1i ⊢ ( ⊤ → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
5 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
6 ax-resscn ⊢ ℝ ⊆ ℂ
7 5 6 sstri ⊢ ( 0 [,] 1 ) ⊆ ℂ
8 7 a1i ⊢ ( ⊤ → ( 0 [,] 1 ) ⊆ ℂ )
9 ax-mulf ⊢ · : ( ℂ × ℂ ) ⟶ ℂ
10 ffn ⊢ ( · : ( ℂ × ℂ ) ⟶ ℂ → · Fn ( ℂ × ℂ ) )
11 9 10 ax-mp ⊢ · Fn ( ℂ × ℂ )
12 fnov ⊢ ( · Fn ( ℂ × ℂ ) ↔ · = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) )
13 11 12 mpbi ⊢ · = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) )
14 1 mulcn ⊢ · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
15 13 14 eqeltrri ⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
16 15 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
17 2 4 8 2 4 8 16 cnmpt2res ⊢ ( ⊤ → ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( TopOpen ‘ ℂfld ) ) )
18 17 mptru ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( TopOpen ‘ ℂfld ) )
19 iimulcl ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) → ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 ) )
20 19 rgen2 ⊢ ∀ 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 )
21 eqid ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) )
22 21 fmpo ⊢ ( ∀ 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 ) ↔ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ( 0 [,] 1 ) )
23 frn ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ ( 0 [,] 1 ) → ran ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( 0 [,] 1 ) )
24 22 23 sylbi ⊢ ( ∀ 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( 𝑥 · 𝑦 ) ∈ ( 0 [,] 1 ) → ran ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( 0 [,] 1 ) )
25 20 24 ax-mp ⊢ ran ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( 0 [,] 1 )
26 cnrest2 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( 0 [,] 1 ) ∧ ( 0 [,] 1 ) ⊆ ℂ ) → ( ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) ) ) )
27 3 25 7 26 mp3an ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) ) )
28 18 27 mpbi ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) )
29 2 oveq2i ⊢ ( ( II ×t II ) Cn II ) = ( ( II ×t II ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) )
30 28 29 eleqtrri ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( II ×t II ) Cn II )