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 ∧ 𝑘 < ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) )