This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )