Theorem uzub

Description: A set of reals, indexed by upper integers, is bound if and only if any upper part is bound. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	uzub.1	$$⊢Ⅎj\phi$$
	uzub.2	$$⊢\phi \to M\in \mathbb{Z}$$
	uzub.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	uzub.12	$$⊢\left(\phi \wedge j\in Z\right)\to B\in ℝ$$
Assertion	uzub	$$⊢\phi \to \left(\exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}B\le x\leftrightarrow \exists x\in ℝ\forall j\in ZB\le x\right)$$

Proof

Step	Hyp	Ref	Expression
1		uzub.1	$$⊢Ⅎj\phi$$
2		uzub.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		uzub.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		uzub.12	$$⊢\left(\phi \wedge j\in Z\right)\to B\in ℝ$$
5		fveq2	$$⊢k=i\to {\mathbb{Z}}_{\ge k}={\mathbb{Z}}_{\ge i}$$
6	5	raleqdv	$$⊢k=i\to \left(\forall j\in {\mathbb{Z}}_{\ge k}B\le x\leftrightarrow \forall j\in {\mathbb{Z}}_{\ge i}B\le x\right)$$
7	6	cbvrexvw	$$⊢\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}B\le x\leftrightarrow \exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le x$$
8	7	a1i	$$⊢x=w\to \left(\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}B\le x\leftrightarrow \exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le x\right)$$
9		breq2	$$⊢x=w\to \left(B\le x\leftrightarrow B\le w\right)$$
10	9	ralbidv	$$⊢x=w\to \left(\forall j\in {\mathbb{Z}}_{\ge i}B\le x\leftrightarrow \forall j\in {\mathbb{Z}}_{\ge i}B\le w\right)$$
11	10	rexbidv	$$⊢x=w\to \left(\exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le x\leftrightarrow \exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le w\right)$$
12	8 11	bitrd	$$⊢x=w\to \left(\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}B\le x\leftrightarrow \exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le w\right)$$
13	12	cbvrexvw	$$⊢\exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}B\le x\leftrightarrow \exists w\in ℝ\exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le w$$
14	13	a1i	$$⊢\phi \to \left(\exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}B\le x\leftrightarrow \exists w\in ℝ\exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le w\right)$$
15		breq2	$$⊢w=y\to \left(B\le w\leftrightarrow B\le y\right)$$
16	15	ralbidv	$$⊢w=y\to \left(\forall j\in {\mathbb{Z}}_{\ge i}B\le w\leftrightarrow \forall j\in {\mathbb{Z}}_{\ge i}B\le y\right)$$
17	16	rexbidv	$$⊢w=y\to \left(\exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le w\leftrightarrow \exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le y\right)$$
18	17	cbvrexvw	$$⊢\exists w\in ℝ\exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le w\leftrightarrow \exists y\in ℝ\exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le y$$
19	18	biimpi	$$⊢\exists w\in ℝ\exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le w\to \exists y\in ℝ\exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le y$$
20		nfv	$$⊢Ⅎjy\in ℝ$$
21	1 20	nfan	$$⊢Ⅎj\left(\phi \wedge y\in ℝ\right)$$
22		nfv	$$⊢Ⅎji\in Z$$
23	21 22	nfan	$$⊢Ⅎj\left(\left(\phi \wedge y\in ℝ\right)\wedge i\in Z\right)$$
24		nfra1	$$⊢Ⅎj\forall j\in {\mathbb{Z}}_{\ge i}B\le y$$
25	23 24	nfan	$$⊢Ⅎj\left(\left(\left(\phi \wedge y\in ℝ\right)\wedge i\in Z\right)\wedge \forall j\in {\mathbb{Z}}_{\ge i}B\le y\right)$$
26		nfmpt1	$$⊢\underset{\_}{Ⅎ}j\left(j\in \left(M\dots i\right)⟼B\right)$$
27	26	nfrn	$$⊢\underset{\_}{Ⅎ}j\mathrm{ran}\left(j\in \left(M\dots i\right)⟼B\right)$$
28		nfcv	$$⊢\underset{\_}{Ⅎ}jℝ$$
29		nfcv	$$⊢\underset{\_}{Ⅎ}j<$$
30	27 28 29	nfsup	$$⊢\underset{\_}{Ⅎ}jsup\left(\mathrm{ran}\left(j\in \left(M\dots i\right)⟼B\right),ℝ,<\right)$$
31		nfcv	$$⊢\underset{\_}{Ⅎ}j\le$$
32		nfcv	$$⊢\underset{\_}{Ⅎ}jy$$
33	30 31 32	nfbr	$$⊢Ⅎjsup\left(\mathrm{ran}\left(j\in \left(M\dots i\right)⟼B\right),ℝ,<\right)\le y$$
34	33 32 30	nfif	$$⊢\underset{\_}{Ⅎ}jif\left(sup\left(\mathrm{ran}\left(j\in \left(M\dots i\right)⟼B\right),ℝ,<\right)\le y,y,sup\left(\mathrm{ran}\left(j\in \left(M\dots i\right)⟼B\right),ℝ,<\right)\right)$$
35	2	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge y\in ℝ\right)\wedge i\in Z\right)\wedge \forall j\in {\mathbb{Z}}_{\ge i}B\le y\right)\to M\in \mathbb{Z}$$
36		simpllr	$$⊢\left(\left(\left(\phi \wedge y\in ℝ\right)\wedge i\in Z\right)\wedge \forall j\in {\mathbb{Z}}_{\ge i}B\le y\right)\to y\in ℝ$$
37		eqid	$$⊢sup\left(\mathrm{ran}\left(j\in \left(M\dots i\right)⟼B\right),ℝ,<\right)=sup\left(\mathrm{ran}\left(j\in \left(M\dots i\right)⟼B\right),ℝ,<\right)$$
38		eqid	$$⊢if\left(sup\left(\mathrm{ran}\left(j\in \left(M\dots i\right)⟼B\right),ℝ,<\right)\le y,y,sup\left(\mathrm{ran}\left(j\in \left(M\dots i\right)⟼B\right),ℝ,<\right)\right)=if\left(sup\left(\mathrm{ran}\left(j\in \left(M\dots i\right)⟼B\right),ℝ,<\right)\le y,y,sup\left(\mathrm{ran}\left(j\in \left(M\dots i\right)⟼B\right),ℝ,<\right)\right)$$
39		simplr	$$⊢\left(\left(\left(\phi \wedge y\in ℝ\right)\wedge i\in Z\right)\wedge \forall j\in {\mathbb{Z}}_{\ge i}B\le y\right)\to i\in Z$$
40	4	ad5ant15	$$⊢\left(\left(\left(\left(\phi \wedge y\in ℝ\right)\wedge i\in Z\right)\wedge \forall j\in {\mathbb{Z}}_{\ge i}B\le y\right)\wedge j\in Z\right)\to B\in ℝ$$
41		simpr	$$⊢\left(\left(\left(\phi \wedge y\in ℝ\right)\wedge i\in Z\right)\wedge \forall j\in {\mathbb{Z}}_{\ge i}B\le y\right)\to \forall j\in {\mathbb{Z}}_{\ge i}B\le y$$
42	25 34 35 3 36 37 38 39 40 41	uzublem	$$⊢\left(\left(\left(\phi \wedge y\in ℝ\right)\wedge i\in Z\right)\wedge \forall j\in {\mathbb{Z}}_{\ge i}B\le y\right)\to \exists w\in ℝ\forall j\in ZB\le w$$
43	42	rexlimdva2	$$⊢\left(\phi \wedge y\in ℝ\right)\to \left(\exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le y\to \exists w\in ℝ\forall j\in ZB\le w\right)$$
44	43	imp	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge \exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le y\right)\to \exists w\in ℝ\forall j\in ZB\le w$$
45	44	rexlimdva2	$$⊢\phi \to \left(\exists y\in ℝ\exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le y\to \exists w\in ℝ\forall j\in ZB\le w\right)$$
46	45	imp	$$⊢\left(\phi \wedge \exists y\in ℝ\exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le y\right)\to \exists w\in ℝ\forall j\in ZB\le w$$
47	19 46	sylan2	$$⊢\left(\phi \wedge \exists w\in ℝ\exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le w\right)\to \exists w\in ℝ\forall j\in ZB\le w$$
48	47	ex	$$⊢\phi \to \left(\exists w\in ℝ\exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le w\to \exists w\in ℝ\forall j\in ZB\le w\right)$$
49	2 3	uzidd2	$$⊢\phi \to M\in Z$$
50	49	ad2antrr	$$⊢\left(\left(\phi \wedge w\in ℝ\right)\wedge \forall j\in ZB\le w\right)\to M\in Z$$
51	3	raleqi	$$⊢\forall j\in ZB\le w\leftrightarrow \forall j\in {\mathbb{Z}}_{\ge M}B\le w$$
52	51	bilani	$$⊢\left(\left(\phi \wedge w\in ℝ\right)\wedge \forall j\in ZB\le w\right)\to \forall j\in {\mathbb{Z}}_{\ge M}B\le w$$
53		nfv	$$⊢Ⅎi\forall j\in {\mathbb{Z}}_{\ge M}B\le w$$
54		fveq2	$$⊢i=M\to {\mathbb{Z}}_{\ge i}={\mathbb{Z}}_{\ge M}$$
55	54	raleqdv	$$⊢i=M\to \left(\forall j\in {\mathbb{Z}}_{\ge i}B\le w\leftrightarrow \forall j\in {\mathbb{Z}}_{\ge M}B\le w\right)$$
56	53 55	rspce	$$⊢\left(M\in Z\wedge \forall j\in {\mathbb{Z}}_{\ge M}B\le w\right)\to \exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le w$$
57	50 52 56	syl2anc	$$⊢\left(\left(\phi \wedge w\in ℝ\right)\wedge \forall j\in ZB\le w\right)\to \exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le w$$
58	57	ex	$$⊢\left(\phi \wedge w\in ℝ\right)\to \left(\forall j\in ZB\le w\to \exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le w\right)$$
59	58	reximdva	$$⊢\phi \to \left(\exists w\in ℝ\forall j\in ZB\le w\to \exists w\in ℝ\exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le w\right)$$
60	48 59	impbid	$$⊢\phi \to \left(\exists w\in ℝ\exists i\in Z\forall j\in {\mathbb{Z}}_{\ge i}B\le w\leftrightarrow \exists w\in ℝ\forall j\in ZB\le w\right)$$
61		breq2	$$⊢w=x\to \left(B\le w\leftrightarrow B\le x\right)$$
62	61	ralbidv	$$⊢w=x\to \left(\forall j\in ZB\le w\leftrightarrow \forall j\in ZB\le x\right)$$
63	62	cbvrexvw	$$⊢\exists w\in ℝ\forall j\in ZB\le w\leftrightarrow \exists x\in ℝ\forall j\in ZB\le x$$
64	63	a1i	$$⊢\phi \to \left(\exists w\in ℝ\forall j\in ZB\le w\leftrightarrow \exists x\in ℝ\forall j\in ZB\le x\right)$$
65	14 60 64	3bitrd	$$⊢\phi \to \left(\exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}B\le x\leftrightarrow \exists x\in ℝ\forall j\in ZB\le x\right)$$