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\left(\left(f:\mathbb{N}⟶X\wedge \forall k\in \mathbb{N}L\left(f\left(k\right)\right)\le 1\right)\to \exists k\in \mathbb{N}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:\mathbb{N}⟶X\wedge \forall k\in \mathbb{N}L\left(f\left(k\right)\right)\le 1\right)\to \exists k\in \mathbb{N}M\left(T\left(f\left(k\right)\right)\right)\le k\right)\leftrightarrow \left(f:\mathbb{N}⟶X\to \left(\forall k\in \mathbb{N}L\left(f\left(k\right)\right)\le 1\to \exists k\in \mathbb{N}M\left(T\left(f\left(k\right)\right)\right)\le k\right)\right)$$
9		r19.35	$$⊢\exists k\in \mathbb{N}\left(L\left(f\left(k\right)\right)\le 1\to M\left(T\left(f\left(k\right)\right)\right)\le k\right)\leftrightarrow \left(\forall k\in \mathbb{N}L\left(f\left(k\right)\right)\le 1\to \exists k\in \mathbb{N}M\left(T\left(f\left(k\right)\right)\right)\le k\right)$$
10	9	imbi2i	$$⊢\left(f:\mathbb{N}⟶X\to \exists k\in \mathbb{N}\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)\leftrightarrow \left(f:\mathbb{N}⟶X\to \left(\forall k\in \mathbb{N}L\left(f\left(k\right)\right)\le 1\to \exists k\in \mathbb{N}M\left(T\left(f\left(k\right)\right)\right)\le k\right)\right)$$
11	8 10	bitr4i	$$⊢\left(\left(f:\mathbb{N}⟶X\wedge \forall k\in \mathbb{N}L\left(f\left(k\right)\right)\le 1\right)\to \exists k\in \mathbb{N}M\left(T\left(f\left(k\right)\right)\right)\le k\right)\leftrightarrow \left(f:\mathbb{N}⟶X\to \exists k\in \mathbb{N}\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\left(\left(f:\mathbb{N}⟶X\wedge \forall k\in \mathbb{N}L\left(f\left(k\right)\right)\le 1\right)\to \exists k\in \mathbb{N}M\left(T\left(f\left(k\right)\right)\right)\le k\right)\leftrightarrow \forall f\left(f:\mathbb{N}⟶X\to \exists k\in \mathbb{N}\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	$$⊢\mathbb{N}\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\leftrightarrow 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\leftrightarrow 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)\leftrightarrow \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\left(f:\mathbb{N}⟶X\to \exists k\in \mathbb{N}\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 \mathbb{N}\forall y\in X\left(L\left(y\right)\le 1\to M\left(T\left(y\right)\right)\le k\right)$$
21		nnre	$$⊢k\in \mathbb{N}\to k\in ℝ$$
22	21	anim1i	$$⊢\left(k\in \mathbb{N}\wedge \forall y\in X\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\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 \mathbb{N}\forall y\in X\left(L\left(y\right)\le 1\to M\left(T\left(y\right)\right)\le k\right)\to \exists k\in ℝ\forall y\in X\left(L\left(y\right)\le 1\to M\left(T\left(y\right)\right)\le k\right)$$
24	20 23	syl	$$⊢\forall f\left(f:\mathbb{N}⟶X\to \exists k\in \mathbb{N}\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 ℝ\forall y\in X\left(L\left(y\right)\le 1\to M\left(T\left(y\right)\right)\le k\right)$$
25	12 24	sylbi	$$⊢\forall f\left(\left(f:\mathbb{N}⟶X\wedge \forall k\in \mathbb{N}L\left(f\left(k\right)\right)\le 1\right)\to \exists k\in \mathbb{N}M\left(T\left(f\left(k\right)\right)\right)\le k\right)\to \exists k\in ℝ\forall y\in X\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 ℝ\leftrightarrow \exists k\in ℝ\forall y\in X\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\left(\left(f:\mathbb{N}⟶X\wedge \forall k\in \mathbb{N}L\left(f\left(k\right)\right)\le 1\right)\to \exists k\in \mathbb{N}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\left(\left(f:\mathbb{N}⟶X\wedge \forall k\in \mathbb{N}L\left(f\left(k\right)\right)\le 1\right)\to \exists k\in \mathbb{N}M\left(T\left(f\left(k\right)\right)\right)\le k\right)\right)\to N\left(T\right)\in ℝ$$