Metamath Proof Explorer

Theorem nmobndseqiALT

Description: Alternate shorter proof of nmobndseqi based on Axioms ax-reg and ax-ac2 instead of ax-cc . (Contributed by NM, 18-Jan-2008) (New usage is discouraged.) (Proof modification 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 nmobndseqiALT ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 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 impexp ⊢ ( ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 ) → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ↔ ( 𝑓 : ℕ ⟶ 𝑋 → ( ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) )
9 r19.35 ⊢ ( ∃ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ↔ ( ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) )
10 9 imbi2i ⊢ ( ( 𝑓 : ℕ ⟶ 𝑋 → ∃ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) ↔ ( 𝑓 : ℕ ⟶ 𝑋 → ( ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) )
11 8 10 bitr4i ⊢ ( ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 ) → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ↔ ( 𝑓 : ℕ ⟶ 𝑋 → ∃ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) )
12 11 albii ⊢ ( ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 ) → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ↔ ∀ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 → ∃ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) )
13 nnex ⊢ ℕ ∈ V
14 fveq2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑘 ) → ( 𝐿 ‘ 𝑦 ) = ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) )
15 14 breq1d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑘 ) → ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ↔ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 ) )
16 fveq2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑘 ) → ( 𝑇 ‘ 𝑦 ) = ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) )
17 16 fveq2d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑘 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) )
18 17 breq1d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑘 ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ↔ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) )
19 15 18 imbi12d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑘 ) → ( ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) ↔ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) )
20 13 19 ac6n ⊢ ( ∀ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 → ∃ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) → ∃ 𝑘 ∈ ℕ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) )
21 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
22 21 anim1i ⊢ ( ( 𝑘 ∈ ℕ ∧ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) ) → ( 𝑘 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) ) )
23 22 reximi2 ⊢ ( ∃ 𝑘 ∈ ℕ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) )
24 20 23 syl ⊢ ( ∀ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 → ∃ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) )
25 12 24 sylbi ⊢ ( ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 ) → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) )
26 1 2 3 4 5 6 7 nmobndi ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) ) )
27 25 26 syl5ibr ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 ) → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ ) )
28 27 imp ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 ) → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ )