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	\|- F/ j ph
	uzub.2	\|- ( ph -> M e. ZZ )
	uzub.3	\|- Z = ( ZZ>= ` M )
	uzub.12	\|- ( ( ph /\ j e. Z ) -> B e. RR )
Assertion	uzub	\|- ( ph -> ( E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) B <_ x <-> E. x e. RR A. j e. Z B <_ x ) )

Proof

Step	Hyp	Ref	Expression
1		uzub.1	\|- F/ j ph
2		uzub.2	\|- ( ph -> M e. ZZ )
3		uzub.3	\|- Z = ( ZZ>= ` M )
4		uzub.12	\|- ( ( ph /\ j e. Z ) -> B e. RR )
5		fveq2	\|- ( k = i -> ( ZZ>= ` k ) = ( ZZ>= ` i ) )
6	5	raleqdv	\|- ( k = i -> ( A. j e. ( ZZ>= ` k ) B <_ x <-> A. j e. ( ZZ>= ` i ) B <_ x ) )
7	6	cbvrexvw	\|- ( E. k e. Z A. j e. ( ZZ>= ` k ) B <_ x <-> E. i e. Z A. j e. ( ZZ>= ` i ) B <_ x )
8	7	a1i	\|- ( x = w -> ( E. k e. Z A. j e. ( ZZ>= ` k ) B <_ x <-> E. i e. Z A. j e. ( ZZ>= ` i ) B <_ x ) )
9		breq2	\|- ( x = w -> ( B <_ x <-> B <_ w ) )
10	9	ralbidv	\|- ( x = w -> ( A. j e. ( ZZ>= ` i ) B <_ x <-> A. j e. ( ZZ>= ` i ) B <_ w ) )
11	10	rexbidv	\|- ( x = w -> ( E. i e. Z A. j e. ( ZZ>= ` i ) B <_ x <-> E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w ) )
12	8 11	bitrd	\|- ( x = w -> ( E. k e. Z A. j e. ( ZZ>= ` k ) B <_ x <-> E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w ) )
13	12	cbvrexvw	\|- ( E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) B <_ x <-> E. w e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w )
14	13	a1i	\|- ( ph -> ( E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) B <_ x <-> E. w e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w ) )
15		breq2	\|- ( w = y -> ( B <_ w <-> B <_ y ) )
16	15	ralbidv	\|- ( w = y -> ( A. j e. ( ZZ>= ` i ) B <_ w <-> A. j e. ( ZZ>= ` i ) B <_ y ) )
17	16	rexbidv	\|- ( w = y -> ( E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w <-> E. i e. Z A. j e. ( ZZ>= ` i ) B <_ y ) )
18	17	cbvrexvw	\|- ( E. w e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w <-> E. y e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ y )
19	18	biimpi	\|- ( E. w e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w -> E. y e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ y )
20		nfv	\|- F/ j y e. RR
21	1 20	nfan	\|- F/ j ( ph /\ y e. RR )
22		nfv	\|- F/ j i e. Z
23	21 22	nfan	\|- F/ j ( ( ph /\ y e. RR ) /\ i e. Z )
24		nfra1	\|- F/ j A. j e. ( ZZ>= ` i ) B <_ y
25	23 24	nfan	\|- F/ j ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ A. j e. ( ZZ>= ` i ) B <_ y )
26		nfmpt1	\|- F/_ j ( j e. ( M ... i ) \|-> B )
27	26	nfrn	\|- F/_ j ran ( j e. ( M ... i ) \|-> B )
28		nfcv	\|- F/_ j RR
29		nfcv	\|- F/_ j <
30	27 28 29	nfsup	\|- F/_ j sup ( ran ( j e. ( M ... i ) \|-> B ) , RR , < )
31		nfcv	\|- F/_ j <_
32		nfcv	\|- F/_ j y
33	30 31 32	nfbr	\|- F/ j sup ( ran ( j e. ( M ... i ) \|-> B ) , RR , < ) <_ y
34	33 32 30	nfif	\|- F/_ j if ( sup ( ran ( j e. ( M ... i ) \|-> B ) , RR , < ) <_ y , y , sup ( ran ( j e. ( M ... i ) \|-> B ) , RR , < ) )
35	2	ad3antrrr	\|- ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ A. j e. ( ZZ>= ` i ) B <_ y ) -> M e. ZZ )
36		simpllr	\|- ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ A. j e. ( ZZ>= ` i ) B <_ y ) -> y e. RR )
37		eqid	\|- sup ( ran ( j e. ( M ... i ) \|-> B ) , RR , < ) = sup ( ran ( j e. ( M ... i ) \|-> B ) , RR , < )
38		eqid	\|- if ( sup ( ran ( j e. ( M ... i ) \|-> B ) , RR , < ) <_ y , y , sup ( ran ( j e. ( M ... i ) \|-> B ) , RR , < ) ) = if ( sup ( ran ( j e. ( M ... i ) \|-> B ) , RR , < ) <_ y , y , sup ( ran ( j e. ( M ... i ) \|-> B ) , RR , < ) )
39		simplr	\|- ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ A. j e. ( ZZ>= ` i ) B <_ y ) -> i e. Z )
40	4	ad5ant15	\|- ( ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ A. j e. ( ZZ>= ` i ) B <_ y ) /\ j e. Z ) -> B e. RR )
41		simpr	\|- ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ A. j e. ( ZZ>= ` i ) B <_ y ) -> A. j e. ( ZZ>= ` i ) B <_ y )
42	25 34 35 3 36 37 38 39 40 41	uzublem	\|- ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ A. j e. ( ZZ>= ` i ) B <_ y ) -> E. w e. RR A. j e. Z B <_ w )
43	42	rexlimdva2	\|- ( ( ph /\ y e. RR ) -> ( E. i e. Z A. j e. ( ZZ>= ` i ) B <_ y -> E. w e. RR A. j e. Z B <_ w ) )
44	43	imp	\|- ( ( ( ph /\ y e. RR ) /\ E. i e. Z A. j e. ( ZZ>= ` i ) B <_ y ) -> E. w e. RR A. j e. Z B <_ w )
45	44	rexlimdva2	\|- ( ph -> ( E. y e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ y -> E. w e. RR A. j e. Z B <_ w ) )
46	45	imp	\|- ( ( ph /\ E. y e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ y ) -> E. w e. RR A. j e. Z B <_ w )
47	19 46	sylan2	\|- ( ( ph /\ E. w e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w ) -> E. w e. RR A. j e. Z B <_ w )
48	47	ex	\|- ( ph -> ( E. w e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w -> E. w e. RR A. j e. Z B <_ w ) )
49	2 3	uzidd2	\|- ( ph -> M e. Z )
50	49	ad2antrr	\|- ( ( ( ph /\ w e. RR ) /\ A. j e. Z B <_ w ) -> M e. Z )
51	3	raleqi	\|- ( A. j e. Z B <_ w <-> A. j e. ( ZZ>= ` M ) B <_ w )
52	51	biimpi	\|- ( A. j e. Z B <_ w -> A. j e. ( ZZ>= ` M ) B <_ w )
53	52	adantl	\|- ( ( ( ph /\ w e. RR ) /\ A. j e. Z B <_ w ) -> A. j e. ( ZZ>= ` M ) B <_ w )
54		nfv	\|- F/ i A. j e. ( ZZ>= ` M ) B <_ w
55		fveq2	\|- ( i = M -> ( ZZ>= ` i ) = ( ZZ>= ` M ) )
56	55	raleqdv	\|- ( i = M -> ( A. j e. ( ZZ>= ` i ) B <_ w <-> A. j e. ( ZZ>= ` M ) B <_ w ) )
57	54 56	rspce	\|- ( ( M e. Z /\ A. j e. ( ZZ>= ` M ) B <_ w ) -> E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w )
58	50 53 57	syl2anc	\|- ( ( ( ph /\ w e. RR ) /\ A. j e. Z B <_ w ) -> E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w )
59	58	ex	\|- ( ( ph /\ w e. RR ) -> ( A. j e. Z B <_ w -> E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w ) )
60	59	reximdva	\|- ( ph -> ( E. w e. RR A. j e. Z B <_ w -> E. w e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w ) )
61	48 60	impbid	\|- ( ph -> ( E. w e. RR E. i e. Z A. j e. ( ZZ>= ` i ) B <_ w <-> E. w e. RR A. j e. Z B <_ w ) )
62		breq2	\|- ( w = x -> ( B <_ w <-> B <_ x ) )
63	62	ralbidv	\|- ( w = x -> ( A. j e. Z B <_ w <-> A. j e. Z B <_ x ) )
64	63	cbvrexvw	\|- ( E. w e. RR A. j e. Z B <_ w <-> E. x e. RR A. j e. Z B <_ x )
65	64	a1i	\|- ( ph -> ( E. w e. RR A. j e. Z B <_ w <-> E. x e. RR A. j e. Z B <_ x ) )
66	14 61 65	3bitrd	\|- ( ph -> ( E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) B <_ x <-> E. x e. RR A. j e. Z B <_ x ) )

Metamath Proof Explorer

Theorem uzub

Proof