Metamath Proof Explorer

Theorem nmounbseqiALT

Description: Alternate shorter proof of nmounbseqi based on axioms ax-reg and ax-ac2 instead of ax-cc . (Contributed by NM, 11-Jan-2008) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses nmoubi.1 ⊢ X = BaseSet ⁡ U
nmoubi.y ⊢ Y = BaseSet ⁡ W
nmoubi.l ⊢ L = norm CV ⁡ U
nmoubi.m ⊢ M = norm CV ⁡ W
nmoubi.3 ⊢ N = U normOp OLD W
nmoubi.u ⊢ U ∈ NrmCVec
nmoubi.w ⊢ W ∈ NrmCVec
Assertion nmounbseqiALT ⊢ T : X ⟶ Y ∧ N ⁡ T = +∞ → ∃ f f : ℕ ⟶ X ∧ ∀ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 ∧ k < M ⁡ T ⁡ f ⁡ k

Proof

Step Hyp Ref Expression
1 nmoubi.1 ⊢ X = BaseSet ⁡ U
2 nmoubi.y ⊢ Y = BaseSet ⁡ W
3 nmoubi.l ⊢ L = norm CV ⁡ U
4 nmoubi.m ⊢ M = norm CV ⁡ W
5 nmoubi.3 ⊢ N = U normOp OLD W
6 nmoubi.u ⊢ U ∈ NrmCVec
7 nmoubi.w ⊢ W ∈ NrmCVec
8 1 2 3 4 5 6 7 nmounbi ⊢ T : X ⟶ Y → N ⁡ T = +∞ ↔ ∀ k ∈ ℝ ∃ y ∈ X L ⁡ y ≤ 1 ∧ k < M ⁡ T ⁡ y
9 8 biimpa ⊢ T : X ⟶ Y ∧ N ⁡ T = +∞ → ∀ k ∈ ℝ ∃ y ∈ X L ⁡ y ≤ 1 ∧ k < M ⁡ T ⁡ y
10 nnre ⊢ k ∈ ℕ → k ∈ ℝ
11 10 imim1i ⊢ k ∈ ℝ → ∃ y ∈ X L ⁡ y ≤ 1 ∧ k < M ⁡ T ⁡ y → k ∈ ℕ → ∃ y ∈ X L ⁡ y ≤ 1 ∧ k < M ⁡ T ⁡ y
12 11 ralimi2 ⊢ ∀ k ∈ ℝ ∃ y ∈ X L ⁡ y ≤ 1 ∧ k < M ⁡ T ⁡ y → ∀ k ∈ ℕ ∃ y ∈ X L ⁡ y ≤ 1 ∧ k < M ⁡ T ⁡ y
13 nnex ⊢ ℕ ∈ V
14 fveq2 ⊢ y = f ⁡ k → L ⁡ y = L ⁡ f ⁡ k
15 14 breq1d ⊢ y = f ⁡ k → L ⁡ y ≤ 1 ↔ L ⁡ f ⁡ k ≤ 1
16 fveq2 ⊢ y = f ⁡ k → T ⁡ y = T ⁡ f ⁡ k
17 16 fveq2d ⊢ y = f ⁡ k → M ⁡ T ⁡ y = M ⁡ T ⁡ f ⁡ k
18 17 breq2d ⊢ y = f ⁡ k → k < M ⁡ T ⁡ y ↔ k < M ⁡ T ⁡ f ⁡ k
19 15 18 anbi12d ⊢ y = f ⁡ k → L ⁡ y ≤ 1 ∧ k < M ⁡ T ⁡ y ↔ L ⁡ f ⁡ k ≤ 1 ∧ k < M ⁡ T ⁡ f ⁡ k
20 13 19 ac6s ⊢ ∀ k ∈ ℕ ∃ y ∈ X L ⁡ y ≤ 1 ∧ k < M ⁡ T ⁡ y → ∃ f f : ℕ ⟶ X ∧ ∀ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 ∧ k < M ⁡ T ⁡ f ⁡ k
21 9 12 20 3syl ⊢ T : X ⟶ Y ∧ N ⁡ T = +∞ → ∃ f f : ℕ ⟶ X ∧ ∀ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 ∧ k < M ⁡ T ⁡ f ⁡ k