# 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 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
nmoubi.y ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
nmoubi.l ${⊢}{L}={norm}_{CV}\left({U}\right)$
nmoubi.m ${⊢}{M}={norm}_{CV}\left({W}\right)$
nmoubi.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
nmoubi.u ${⊢}{U}\in \mathrm{NrmCVec}$
nmoubi.w ${⊢}{W}\in \mathrm{NrmCVec}$
Assertion nmobndseqiALT ${⊢}\left({T}:{X}⟶{Y}\wedge \forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)\to {N}\left({T}\right)\in ℝ$

### Proof

Step Hyp Ref Expression
1 nmoubi.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 nmoubi.y ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
3 nmoubi.l ${⊢}{L}={norm}_{CV}\left({U}\right)$
4 nmoubi.m ${⊢}{M}={norm}_{CV}\left({W}\right)$
5 nmoubi.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
6 nmoubi.u ${⊢}{U}\in \mathrm{NrmCVec}$
7 nmoubi.w ${⊢}{W}\in \mathrm{NrmCVec}$
8 impexp ${⊢}\left(\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)↔\left({f}:ℕ⟶{X}\to \left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)$
9 r19.35 ${⊢}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)↔\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)$
10 9 imbi2i ${⊢}\left({f}:ℕ⟶{X}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)↔\left({f}:ℕ⟶{X}\to \left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)$
11 8 10 bitr4i ${⊢}\left(\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)↔\left({f}:ℕ⟶{X}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)$
12 11 albii ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)↔\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)$
13 nnex ${⊢}ℕ\in \mathrm{V}$
14 fveq2 ${⊢}{y}={f}\left({k}\right)\to {L}\left({y}\right)={L}\left({f}\left({k}\right)\right)$
15 14 breq1d ${⊢}{y}={f}\left({k}\right)\to \left({L}\left({y}\right)\le 1↔{L}\left({f}\left({k}\right)\right)\le 1\right)$
16 fveq2 ${⊢}{y}={f}\left({k}\right)\to {T}\left({y}\right)={T}\left({f}\left({k}\right)\right)$
17 16 fveq2d ${⊢}{y}={f}\left({k}\right)\to {M}\left({T}\left({y}\right)\right)={M}\left({T}\left({f}\left({k}\right)\right)\right)$
18 17 breq1d ${⊢}{y}={f}\left({k}\right)\to \left({M}\left({T}\left({y}\right)\right)\le {k}↔{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)$
19 15 18 imbi12d ${⊢}{y}={f}\left({k}\right)\to \left(\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)↔\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)$
20 13 19 ac6n ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)$
21 nnre ${⊢}{k}\in ℕ\to {k}\in ℝ$
22 21 anim1i ${⊢}\left({k}\in ℕ\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)\right)\to \left({k}\in ℝ\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)\right)$
23 22 reximi2 ${⊢}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)\to \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)$
24 20 23 syl ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\to {M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)\to \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)$
25 12 24 sylbi ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\to \exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)$
26 1 2 3 4 5 6 7 nmobndi ${⊢}{T}:{X}⟶{Y}\to \left({N}\left({T}\right)\in ℝ↔\exists {k}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {k}\right)\right)$
27 25 26 syl5ibr ${⊢}{T}:{X}⟶{Y}\to \left(\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\to {N}\left({T}\right)\in ℝ\right)$
28 27 imp ${⊢}\left({T}:{X}⟶{Y}\wedge \forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{L}\left({f}\left({k}\right)\right)\le 1\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({f}\left({k}\right)\right)\right)\le {k}\right)\right)\to {N}\left({T}\right)\in ℝ$