# 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}=\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 nmounbseqiALT ${⊢}\left({T}:{X}⟶{Y}\wedge {N}\left({T}\right)=\mathrm{+\infty }\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\wedge {k}<{M}\left({T}\left({f}\left({k}\right)\right)\right)\right)\right)$

### 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 1 2 3 4 5 6 7 nmounbi ${⊢}{T}:{X}⟶{Y}\to \left({N}\left({T}\right)=\mathrm{+\infty }↔\forall {k}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\wedge {k}<{M}\left({T}\left({y}\right)\right)\right)\right)$
9 8 biimpa ${⊢}\left({T}:{X}⟶{Y}\wedge {N}\left({T}\right)=\mathrm{+\infty }\right)\to \forall {k}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\wedge {k}<{M}\left({T}\left({y}\right)\right)\right)$
10 nnre ${⊢}{k}\in ℕ\to {k}\in ℝ$
11 10 imim1i ${⊢}\left({k}\in ℝ\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\wedge {k}<{M}\left({T}\left({y}\right)\right)\right)\right)\to \left({k}\in ℕ\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\wedge {k}<{M}\left({T}\left({y}\right)\right)\right)\right)$
12 11 ralimi2 ${⊢}\forall {k}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\wedge {k}<{M}\left({T}\left({y}\right)\right)\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\wedge {k}<{M}\left({T}\left({y}\right)\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 breq2d ${⊢}{y}={f}\left({k}\right)\to \left({k}<{M}\left({T}\left({y}\right)\right)↔{k}<{M}\left({T}\left({f}\left({k}\right)\right)\right)\right)$
19 15 18 anbi12d ${⊢}{y}={f}\left({k}\right)\to \left(\left({L}\left({y}\right)\le 1\wedge {k}<{M}\left({T}\left({y}\right)\right)\right)↔\left({L}\left({f}\left({k}\right)\right)\le 1\wedge {k}<{M}\left({T}\left({f}\left({k}\right)\right)\right)\right)\right)$
20 13 19 ac6s ${⊢}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\wedge {k}<{M}\left({T}\left({y}\right)\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\wedge {k}<{M}\left({T}\left({f}\left({k}\right)\right)\right)\right)\right)$
21 9 12 20 3syl ${⊢}\left({T}:{X}⟶{Y}\wedge {N}\left({T}\right)=\mathrm{+\infty }\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶{X}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({L}\left({f}\left({k}\right)\right)\le 1\wedge {k}<{M}\left({T}\left({f}\left({k}\right)\right)\right)\right)\right)$