Metamath Proof Explorer


Theorem nmounbseqi

Description: An unbounded operator determines an unbounded sequence. (Contributed by NM, 11-Jan-2008) (Revised by Mario Carneiro, 7-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmoubi.1 𝑋 = ( BaseSet ‘ 𝑈 )
nmoubi.y 𝑌 = ( BaseSet ‘ 𝑊 )
nmoubi.l 𝐿 = ( normCV𝑈 )
nmoubi.m 𝑀 = ( normCV𝑊 )
nmoubi.3 𝑁 = ( 𝑈 normOpOLD 𝑊 )
nmoubi.u 𝑈 ∈ NrmCVec
nmoubi.w 𝑊 ∈ NrmCVec
Assertion nmounbseqi ( ( 𝑇 : 𝑋𝑌 ∧ ( 𝑁𝑇 ) = +∞ ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓𝑘 ) ) ≤ 1 ∧ 𝑘 < ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓𝑘 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 nmoubi.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 nmoubi.y 𝑌 = ( BaseSet ‘ 𝑊 )
3 nmoubi.l 𝐿 = ( normCV𝑈 )
4 nmoubi.m 𝑀 = ( normCV𝑊 )
5 nmoubi.3 𝑁 = ( 𝑈 normOpOLD 𝑊 )
6 nmoubi.u 𝑈 ∈ NrmCVec
7 nmoubi.w 𝑊 ∈ NrmCVec
8 1 2 3 4 5 6 7 nmounbi ( 𝑇 : 𝑋𝑌 → ( ( 𝑁𝑇 ) = +∞ ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑦𝑋 ( ( 𝐿𝑦 ) ≤ 1 ∧ 𝑘 < ( 𝑀 ‘ ( 𝑇𝑦 ) ) ) ) )
9 8 biimpa ( ( 𝑇 : 𝑋𝑌 ∧ ( 𝑁𝑇 ) = +∞ ) → ∀ 𝑘 ∈ ℝ ∃ 𝑦𝑋 ( ( 𝐿𝑦 ) ≤ 1 ∧ 𝑘 < ( 𝑀 ‘ ( 𝑇𝑦 ) ) ) )
10 nnre ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
11 10 imim1i ( ( 𝑘 ∈ ℝ → ∃ 𝑦𝑋 ( ( 𝐿𝑦 ) ≤ 1 ∧ 𝑘 < ( 𝑀 ‘ ( 𝑇𝑦 ) ) ) ) → ( 𝑘 ∈ ℕ → ∃ 𝑦𝑋 ( ( 𝐿𝑦 ) ≤ 1 ∧ 𝑘 < ( 𝑀 ‘ ( 𝑇𝑦 ) ) ) ) )
12 11 ralimi2 ( ∀ 𝑘 ∈ ℝ ∃ 𝑦𝑋 ( ( 𝐿𝑦 ) ≤ 1 ∧ 𝑘 < ( 𝑀 ‘ ( 𝑇𝑦 ) ) ) → ∀ 𝑘 ∈ ℕ ∃ 𝑦𝑋 ( ( 𝐿𝑦 ) ≤ 1 ∧ 𝑘 < ( 𝑀 ‘ ( 𝑇𝑦 ) ) ) )
13 1 fvexi 𝑋 ∈ V
14 nnenom ℕ ≈ ω
15 fveq2 ( 𝑦 = ( 𝑓𝑘 ) → ( 𝐿𝑦 ) = ( 𝐿 ‘ ( 𝑓𝑘 ) ) )
16 15 breq1d ( 𝑦 = ( 𝑓𝑘 ) → ( ( 𝐿𝑦 ) ≤ 1 ↔ ( 𝐿 ‘ ( 𝑓𝑘 ) ) ≤ 1 ) )
17 2fveq3 ( 𝑦 = ( 𝑓𝑘 ) → ( 𝑀 ‘ ( 𝑇𝑦 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓𝑘 ) ) ) )
18 17 breq2d ( 𝑦 = ( 𝑓𝑘 ) → ( 𝑘 < ( 𝑀 ‘ ( 𝑇𝑦 ) ) ↔ 𝑘 < ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓𝑘 ) ) ) ) )
19 16 18 anbi12d ( 𝑦 = ( 𝑓𝑘 ) → ( ( ( 𝐿𝑦 ) ≤ 1 ∧ 𝑘 < ( 𝑀 ‘ ( 𝑇𝑦 ) ) ) ↔ ( ( 𝐿 ‘ ( 𝑓𝑘 ) ) ≤ 1 ∧ 𝑘 < ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓𝑘 ) ) ) ) ) )
20 13 14 19 axcc4 ( ∀ 𝑘 ∈ ℕ ∃ 𝑦𝑋 ( ( 𝐿𝑦 ) ≤ 1 ∧ 𝑘 < ( 𝑀 ‘ ( 𝑇𝑦 ) ) ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓𝑘 ) ) ≤ 1 ∧ 𝑘 < ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓𝑘 ) ) ) ) ) )
21 9 12 20 3syl ( ( 𝑇 : 𝑋𝑌 ∧ ( 𝑁𝑇 ) = +∞ ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓𝑘 ) ) ≤ 1 ∧ 𝑘 < ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓𝑘 ) ) ) ) ) )