Theorem supcvg

Description: Extract a sequence f in X such that the image of the points in the bounded set A converges to the supremum S of the set. Similar to Equation 4 of Kreyszig p. 144. The proof uses countable choice ax-cc . (Contributed by Mario Carneiro, 15-Feb-2013) (Proof shortened by Mario Carneiro, 26-Apr-2014)

	Ref	Expression
Hypotheses	supcvg.1	|- X e. _V
	supcvg.2	|- S = sup ( A , RR , < )
	supcvg.3	|- R = ( n e. NN |-> ( S - ( 1 / n ) ) )
	supcvg.4	|- ( ph -> X =/= (/) )
	supcvg.5	|- ( ph -> F : X -onto-> A )
	supcvg.6	|- ( ph -> A C_ RR )
	supcvg.7	|- ( ph -> E. x e. RR A. y e. A y <_ x )
Assertion	supcvg	|- ( ph -> E. f ( f : NN --> X /\ ( F o. f ) ~~> S ) )

Proof

Step	Hyp	Ref	Expression
1		supcvg.1	|- X e. _V
2		supcvg.2	|- S = sup ( A , RR , < )
3		supcvg.3	|- R = ( n e. NN |-> ( S - ( 1 / n ) ) )
4		supcvg.4	|- ( ph -> X =/= (/) )
5		supcvg.5	|- ( ph -> F : X -onto-> A )
6		supcvg.6	|- ( ph -> A C_ RR )
7		supcvg.7	|- ( ph -> E. x e. RR A. y e. A y <_ x )
8		oveq2	|- ( n = k -> ( 1 / n ) = ( 1 / k ) )
9	8	oveq2d	|- ( n = k -> ( S - ( 1 / n ) ) = ( S - ( 1 / k ) ) )
10		ovex	|- ( S - ( 1 / k ) ) e. _V
11	9 3 10	fvmpt	|- ( k e. NN -> ( R ` k ) = ( S - ( 1 / k ) ) )
12	11	adantl	|- ( ( ph /\ k e. NN ) -> ( R ` k ) = ( S - ( 1 / k ) ) )
13		fof	|- ( F : X -onto-> A -> F : X --> A )
14	5 13	syl	|- ( ph -> F : X --> A )
15		feq3	|- ( A = (/) -> ( F : X --> A <-> F : X --> (/) ) )
16	14 15	syl5ibcom	|- ( ph -> ( A = (/) -> F : X --> (/) ) )
17		f00	|- ( F : X --> (/) <-> ( F = (/) /\ X = (/) ) )
18	17	simprbi	|- ( F : X --> (/) -> X = (/) )
19	16 18	syl6	|- ( ph -> ( A = (/) -> X = (/) ) )
20	19	necon3d	|- ( ph -> ( X =/= (/) -> A =/= (/) ) )
21	4 20	mpd	|- ( ph -> A =/= (/) )
22	6 21 7	suprcld	|- ( ph -> sup ( A , RR , < ) e. RR )
23	2 22	eqeltrid	|- ( ph -> S e. RR )
24		nnrp	|- ( k e. NN -> k e. RR+ )
25	24	rpreccld	|- ( k e. NN -> ( 1 / k ) e. RR+ )
26		ltsubrp	|- ( ( S e. RR /\ ( 1 / k ) e. RR+ ) -> ( S - ( 1 / k ) ) < S )
27	23 25 26	syl2an	|- ( ( ph /\ k e. NN ) -> ( S - ( 1 / k ) ) < S )
28	12 27	eqbrtrd	|- ( ( ph /\ k e. NN ) -> ( R ` k ) < S )
29	28 2	breqtrdi	|- ( ( ph /\ k e. NN ) -> ( R ` k ) < sup ( A , RR , < ) )
30	6 21 7	3jca	|- ( ph -> ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) )
31		nnrecre	|- ( n e. NN -> ( 1 / n ) e. RR )
32		resubcl	|- ( ( S e. RR /\ ( 1 / n ) e. RR ) -> ( S - ( 1 / n ) ) e. RR )
33	23 31 32	syl2an	|- ( ( ph /\ n e. NN ) -> ( S - ( 1 / n ) ) e. RR )
34	33 3	fmptd	|- ( ph -> R : NN --> RR )
35	34	ffvelcdmda	|- ( ( ph /\ k e. NN ) -> ( R ` k ) e. RR )
36		suprlub	|- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( R ` k ) e. RR ) -> ( ( R ` k ) < sup ( A , RR , < ) <-> E. z e. A ( R ` k ) < z ) )
37	30 35 36	syl2an2r	|- ( ( ph /\ k e. NN ) -> ( ( R ` k ) < sup ( A , RR , < ) <-> E. z e. A ( R ` k ) < z ) )
38	29 37	mpbid	|- ( ( ph /\ k e. NN ) -> E. z e. A ( R ` k ) < z )
39	6	adantr	|- ( ( ph /\ k e. NN ) -> A C_ RR )
40	39	sselda	|- ( ( ( ph /\ k e. NN ) /\ z e. A ) -> z e. RR )
41		ltle	|- ( ( ( R ` k ) e. RR /\ z e. RR ) -> ( ( R ` k ) < z -> ( R ` k ) <_ z ) )
42	35 40 41	syl2an2r	|- ( ( ( ph /\ k e. NN ) /\ z e. A ) -> ( ( R ` k ) < z -> ( R ` k ) <_ z ) )
43	42	reximdva	|- ( ( ph /\ k e. NN ) -> ( E. z e. A ( R ` k ) < z -> E. z e. A ( R ` k ) <_ z ) )
44	38 43	mpd	|- ( ( ph /\ k e. NN ) -> E. z e. A ( R ` k ) <_ z )
45		forn	|- ( F : X -onto-> A -> ran F = A )
46	5 45	syl	|- ( ph -> ran F = A )
47	46	rexeqdv	|- ( ph -> ( E. z e. ran F ( R ` k ) <_ z <-> E. z e. A ( R ` k ) <_ z ) )
48		ffn	|- ( F : X --> A -> F Fn X )
49		breq2	|- ( z = ( F ` x ) -> ( ( R ` k ) <_ z <-> ( R ` k ) <_ ( F ` x ) ) )
50	49	rexrn	|- ( F Fn X -> ( E. z e. ran F ( R ` k ) <_ z <-> E. x e. X ( R ` k ) <_ ( F ` x ) ) )
51	14 48 50	3syl	|- ( ph -> ( E. z e. ran F ( R ` k ) <_ z <-> E. x e. X ( R ` k ) <_ ( F ` x ) ) )
52	47 51	bitr3d	|- ( ph -> ( E. z e. A ( R ` k ) <_ z <-> E. x e. X ( R ` k ) <_ ( F ` x ) ) )
53	52	adantr	|- ( ( ph /\ k e. NN ) -> ( E. z e. A ( R ` k ) <_ z <-> E. x e. X ( R ` k ) <_ ( F ` x ) ) )
54	44 53	mpbid	|- ( ( ph /\ k e. NN ) -> E. x e. X ( R ` k ) <_ ( F ` x ) )
55	54	ralrimiva	|- ( ph -> A. k e. NN E. x e. X ( R ` k ) <_ ( F ` x ) )
56		nnenom	|- NN ~~ _om
57		fveq2	|- ( x = ( f ` k ) -> ( F ` x ) = ( F ` ( f ` k ) ) )
58	57	breq2d	|- ( x = ( f ` k ) -> ( ( R ` k ) <_ ( F ` x ) <-> ( R ` k ) <_ ( F ` ( f ` k ) ) ) )
59	1 56 58	axcc4	|- ( A. k e. NN E. x e. X ( R ` k ) <_ ( F ` x ) -> E. f ( f : NN --> X /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) )
60	55 59	syl	|- ( ph -> E. f ( f : NN --> X /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) )
61		nnuz	|- NN = ( ZZ>= ` 1 )
62		1zzd	|- ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) -> 1 e. ZZ )
63		1zzd	|- ( ph -> 1 e. ZZ )
64	23	recnd	|- ( ph -> S e. CC )
65		1z	|- 1 e. ZZ
66	61	eqimss2i	|- ( ZZ>= ` 1 ) C_ NN
67		nnex	|- NN e. _V
68	66 67	climconst2	|- ( ( S e. CC /\ 1 e. ZZ ) -> ( NN X. { S } ) ~~> S )
69	64 65 68	sylancl	|- ( ph -> ( NN X. { S } ) ~~> S )
70	67	mptex	|- ( n e. NN |-> ( S - ( 1 / n ) ) ) e. _V
71	3 70	eqeltri	|- R e. _V
72	71	a1i	|- ( ph -> R e. _V )
73		ax-1cn	|- 1 e. CC
74		divcnv	|- ( 1 e. CC -> ( n e. NN |-> ( 1 / n ) ) ~~> 0 )
75	73 74	mp1i	|- ( ph -> ( n e. NN |-> ( 1 / n ) ) ~~> 0 )
76		fvconst2g	|- ( ( S e. RR /\ k e. NN ) -> ( ( NN X. { S } ) ` k ) = S )
77	23 76	sylan	|- ( ( ph /\ k e. NN ) -> ( ( NN X. { S } ) ` k ) = S )
78	64	adantr	|- ( ( ph /\ k e. NN ) -> S e. CC )
79	77 78	eqeltrd	|- ( ( ph /\ k e. NN ) -> ( ( NN X. { S } ) ` k ) e. CC )
80		eqid	|- ( n e. NN |-> ( 1 / n ) ) = ( n e. NN |-> ( 1 / n ) )
81		ovex	|- ( 1 / k ) e. _V
82	8 80 81	fvmpt	|- ( k e. NN -> ( ( n e. NN |-> ( 1 / n ) ) ` k ) = ( 1 / k ) )
83	82	adantl	|- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( 1 / n ) ) ` k ) = ( 1 / k ) )
84		nnrecre	|- ( k e. NN -> ( 1 / k ) e. RR )
85	84	recnd	|- ( k e. NN -> ( 1 / k ) e. CC )
86	85	adantl	|- ( ( ph /\ k e. NN ) -> ( 1 / k ) e. CC )
87	83 86	eqeltrd	|- ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( 1 / n ) ) ` k ) e. CC )
88	77 83	oveq12d	|- ( ( ph /\ k e. NN ) -> ( ( ( NN X. { S } ) ` k ) - ( ( n e. NN |-> ( 1 / n ) ) ` k ) ) = ( S - ( 1 / k ) ) )
89	12 88	eqtr4d	|- ( ( ph /\ k e. NN ) -> ( R ` k ) = ( ( ( NN X. { S } ) ` k ) - ( ( n e. NN |-> ( 1 / n ) ) ` k ) ) )
90	61 63 69 72 75 79 87 89	climsub	|- ( ph -> R ~~> ( S - 0 ) )
91	64	subid1d	|- ( ph -> ( S - 0 ) = S )
92	90 91	breqtrd	|- ( ph -> R ~~> S )
93	92	ad2antrr	|- ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) -> R ~~> S )
94	14	ad2antrr	|- ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) -> F : X --> A )
95		fex	|- ( ( F : X --> A /\ X e. _V ) -> F e. _V )
96	94 1 95	sylancl	|- ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) -> F e. _V )
97		vex	|- f e. _V
98		coexg	|- ( ( F e. _V /\ f e. _V ) -> ( F o. f ) e. _V )
99	96 97 98	sylancl	|- ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) -> ( F o. f ) e. _V )
100	34	ad2antrr	|- ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) -> R : NN --> RR )
101	100	ffvelcdmda	|- ( ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) /\ m e. NN ) -> ( R ` m ) e. RR )
102	14 6	fssd	|- ( ph -> F : X --> RR )
103		fco	|- ( ( F : X --> RR /\ f : NN --> X ) -> ( F o. f ) : NN --> RR )
104	102 103	sylan	|- ( ( ph /\ f : NN --> X ) -> ( F o. f ) : NN --> RR )
105	104	adantr	|- ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) -> ( F o. f ) : NN --> RR )
106	105	ffvelcdmda	|- ( ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) /\ m e. NN ) -> ( ( F o. f ) ` m ) e. RR )
107		fveq2	|- ( k = m -> ( R ` k ) = ( R ` m ) )
108		2fveq3	|- ( k = m -> ( F ` ( f ` k ) ) = ( F ` ( f ` m ) ) )
109	107 108	breq12d	|- ( k = m -> ( ( R ` k ) <_ ( F ` ( f ` k ) ) <-> ( R ` m ) <_ ( F ` ( f ` m ) ) ) )
110	109	rspccva	|- ( ( A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) /\ m e. NN ) -> ( R ` m ) <_ ( F ` ( f ` m ) ) )
111	110	adantll	|- ( ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) /\ m e. NN ) -> ( R ` m ) <_ ( F ` ( f ` m ) ) )
112		simplr	|- ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) -> f : NN --> X )
113		fvco3	|- ( ( f : NN --> X /\ m e. NN ) -> ( ( F o. f ) ` m ) = ( F ` ( f ` m ) ) )
114	112 113	sylan	|- ( ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) /\ m e. NN ) -> ( ( F o. f ) ` m ) = ( F ` ( f ` m ) ) )
115	111 114	breqtrrd	|- ( ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) /\ m e. NN ) -> ( R ` m ) <_ ( ( F o. f ) ` m ) )
116	30	ad3antrrr	|- ( ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) /\ m e. NN ) -> ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) )
117	112	ffvelcdmda	|- ( ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) /\ m e. NN ) -> ( f ` m ) e. X )
118	94	ffvelcdmda	|- ( ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) /\ ( f ` m ) e. X ) -> ( F ` ( f ` m ) ) e. A )
119	117 118	syldan	|- ( ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) /\ m e. NN ) -> ( F ` ( f ` m ) ) e. A )
120		suprub	|- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( F ` ( f ` m ) ) e. A ) -> ( F ` ( f ` m ) ) <_ sup ( A , RR , < ) )
121	116 119 120	syl2anc	|- ( ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) /\ m e. NN ) -> ( F ` ( f ` m ) ) <_ sup ( A , RR , < ) )
122	121 2	breqtrrdi	|- ( ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) /\ m e. NN ) -> ( F ` ( f ` m ) ) <_ S )
123	114 122	eqbrtrd	|- ( ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) /\ m e. NN ) -> ( ( F o. f ) ` m ) <_ S )
124	61 62 93 99 101 106 115 123	climsqz	|- ( ( ( ph /\ f : NN --> X ) /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) -> ( F o. f ) ~~> S )
125	124	ex	|- ( ( ph /\ f : NN --> X ) -> ( A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) -> ( F o. f ) ~~> S ) )
126	125	imdistanda	|- ( ph -> ( ( f : NN --> X /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) -> ( f : NN --> X /\ ( F o. f ) ~~> S ) ) )
127	126	eximdv	|- ( ph -> ( E. f ( f : NN --> X /\ A. k e. NN ( R ` k ) <_ ( F ` ( f ` k ) ) ) -> E. f ( f : NN --> X /\ ( F o. f ) ~~> S ) ) )
128	60 127	mpd	|- ( ph -> E. f ( f : NN --> X /\ ( F o. f ) ~~> S ) )