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 𝑋 ∈ V
supcvg.2 𝑆 = sup ( 𝐴 , ℝ , < )
supcvg.3 𝑅 = ( 𝑛 ∈ ℕ ↦ ( 𝑆 − ( 1 / 𝑛 ) ) )
supcvg.4 ( 𝜑𝑋 ≠ ∅ )
supcvg.5 ( 𝜑𝐹 : 𝑋onto𝐴 )
supcvg.6 ( 𝜑𝐴 ⊆ ℝ )
supcvg.7 ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 )
Assertion supcvg ( 𝜑 → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 ∧ ( 𝐹𝑓 ) ⇝ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 supcvg.1 𝑋 ∈ V
2 supcvg.2 𝑆 = sup ( 𝐴 , ℝ , < )
3 supcvg.3 𝑅 = ( 𝑛 ∈ ℕ ↦ ( 𝑆 − ( 1 / 𝑛 ) ) )
4 supcvg.4 ( 𝜑𝑋 ≠ ∅ )
5 supcvg.5 ( 𝜑𝐹 : 𝑋onto𝐴 )
6 supcvg.6 ( 𝜑𝐴 ⊆ ℝ )
7 supcvg.7 ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 )
8 oveq2 ( 𝑛 = 𝑘 → ( 1 / 𝑛 ) = ( 1 / 𝑘 ) )
9 8 oveq2d ( 𝑛 = 𝑘 → ( 𝑆 − ( 1 / 𝑛 ) ) = ( 𝑆 − ( 1 / 𝑘 ) ) )
10 ovex ( 𝑆 − ( 1 / 𝑘 ) ) ∈ V
11 9 3 10 fvmpt ( 𝑘 ∈ ℕ → ( 𝑅𝑘 ) = ( 𝑆 − ( 1 / 𝑘 ) ) )
12 11 adantl ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑅𝑘 ) = ( 𝑆 − ( 1 / 𝑘 ) ) )
13 fof ( 𝐹 : 𝑋onto𝐴𝐹 : 𝑋𝐴 )
14 5 13 syl ( 𝜑𝐹 : 𝑋𝐴 )
15 feq3 ( 𝐴 = ∅ → ( 𝐹 : 𝑋𝐴𝐹 : 𝑋 ⟶ ∅ ) )
16 14 15 syl5ibcom ( 𝜑 → ( 𝐴 = ∅ → 𝐹 : 𝑋 ⟶ ∅ ) )
17 f00 ( 𝐹 : 𝑋 ⟶ ∅ ↔ ( 𝐹 = ∅ ∧ 𝑋 = ∅ ) )
18 17 simprbi ( 𝐹 : 𝑋 ⟶ ∅ → 𝑋 = ∅ )
19 16 18 syl6 ( 𝜑 → ( 𝐴 = ∅ → 𝑋 = ∅ ) )
20 19 necon3d ( 𝜑 → ( 𝑋 ≠ ∅ → 𝐴 ≠ ∅ ) )
21 4 20 mpd ( 𝜑𝐴 ≠ ∅ )
22 6 21 7 suprcld ( 𝜑 → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
23 2 22 eqeltrid ( 𝜑𝑆 ∈ ℝ )
24 nnrp ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ )
25 24 rpreccld ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ+ )
26 ltsubrp ( ( 𝑆 ∈ ℝ ∧ ( 1 / 𝑘 ) ∈ ℝ+ ) → ( 𝑆 − ( 1 / 𝑘 ) ) < 𝑆 )
27 23 25 26 syl2an ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑆 − ( 1 / 𝑘 ) ) < 𝑆 )
28 12 27 eqbrtrd ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑅𝑘 ) < 𝑆 )
29 28 2 breqtrdi ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑅𝑘 ) < sup ( 𝐴 , ℝ , < ) )
30 6 21 7 3jca ( 𝜑 → ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ) )
31 nnrecre ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ )
32 resubcl ( ( 𝑆 ∈ ℝ ∧ ( 1 / 𝑛 ) ∈ ℝ ) → ( 𝑆 − ( 1 / 𝑛 ) ) ∈ ℝ )
33 23 31 32 syl2an ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑆 − ( 1 / 𝑛 ) ) ∈ ℝ )
34 33 3 fmptd ( 𝜑𝑅 : ℕ ⟶ ℝ )
35 34 ffvelrnda ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑅𝑘 ) ∈ ℝ )
36 suprlub ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ) ∧ ( 𝑅𝑘 ) ∈ ℝ ) → ( ( 𝑅𝑘 ) < sup ( 𝐴 , ℝ , < ) ↔ ∃ 𝑧𝐴 ( 𝑅𝑘 ) < 𝑧 ) )
37 30 35 36 syl2an2r ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝑅𝑘 ) < sup ( 𝐴 , ℝ , < ) ↔ ∃ 𝑧𝐴 ( 𝑅𝑘 ) < 𝑧 ) )
38 29 37 mpbid ( ( 𝜑𝑘 ∈ ℕ ) → ∃ 𝑧𝐴 ( 𝑅𝑘 ) < 𝑧 )
39 6 adantr ( ( 𝜑𝑘 ∈ ℕ ) → 𝐴 ⊆ ℝ )
40 39 sselda ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑧𝐴 ) → 𝑧 ∈ ℝ )
41 ltle ( ( ( 𝑅𝑘 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( 𝑅𝑘 ) < 𝑧 → ( 𝑅𝑘 ) ≤ 𝑧 ) )
42 35 40 41 syl2an2r ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑧𝐴 ) → ( ( 𝑅𝑘 ) < 𝑧 → ( 𝑅𝑘 ) ≤ 𝑧 ) )
43 42 reximdva ( ( 𝜑𝑘 ∈ ℕ ) → ( ∃ 𝑧𝐴 ( 𝑅𝑘 ) < 𝑧 → ∃ 𝑧𝐴 ( 𝑅𝑘 ) ≤ 𝑧 ) )
44 38 43 mpd ( ( 𝜑𝑘 ∈ ℕ ) → ∃ 𝑧𝐴 ( 𝑅𝑘 ) ≤ 𝑧 )
45 forn ( 𝐹 : 𝑋onto𝐴 → ran 𝐹 = 𝐴 )
46 5 45 syl ( 𝜑 → ran 𝐹 = 𝐴 )
47 46 rexeqdv ( 𝜑 → ( ∃ 𝑧 ∈ ran 𝐹 ( 𝑅𝑘 ) ≤ 𝑧 ↔ ∃ 𝑧𝐴 ( 𝑅𝑘 ) ≤ 𝑧 ) )
48 ffn ( 𝐹 : 𝑋𝐴𝐹 Fn 𝑋 )
49 breq2 ( 𝑧 = ( 𝐹𝑥 ) → ( ( 𝑅𝑘 ) ≤ 𝑧 ↔ ( 𝑅𝑘 ) ≤ ( 𝐹𝑥 ) ) )
50 49 rexrn ( 𝐹 Fn 𝑋 → ( ∃ 𝑧 ∈ ran 𝐹 ( 𝑅𝑘 ) ≤ 𝑧 ↔ ∃ 𝑥𝑋 ( 𝑅𝑘 ) ≤ ( 𝐹𝑥 ) ) )
51 14 48 50 3syl ( 𝜑 → ( ∃ 𝑧 ∈ ran 𝐹 ( 𝑅𝑘 ) ≤ 𝑧 ↔ ∃ 𝑥𝑋 ( 𝑅𝑘 ) ≤ ( 𝐹𝑥 ) ) )
52 47 51 bitr3d ( 𝜑 → ( ∃ 𝑧𝐴 ( 𝑅𝑘 ) ≤ 𝑧 ↔ ∃ 𝑥𝑋 ( 𝑅𝑘 ) ≤ ( 𝐹𝑥 ) ) )
53 52 adantr ( ( 𝜑𝑘 ∈ ℕ ) → ( ∃ 𝑧𝐴 ( 𝑅𝑘 ) ≤ 𝑧 ↔ ∃ 𝑥𝑋 ( 𝑅𝑘 ) ≤ ( 𝐹𝑥 ) ) )
54 44 53 mpbid ( ( 𝜑𝑘 ∈ ℕ ) → ∃ 𝑥𝑋 ( 𝑅𝑘 ) ≤ ( 𝐹𝑥 ) )
55 54 ralrimiva ( 𝜑 → ∀ 𝑘 ∈ ℕ ∃ 𝑥𝑋 ( 𝑅𝑘 ) ≤ ( 𝐹𝑥 ) )
56 nnenom ℕ ≈ ω
57 fveq2 ( 𝑥 = ( 𝑓𝑘 ) → ( 𝐹𝑥 ) = ( 𝐹 ‘ ( 𝑓𝑘 ) ) )
58 57 breq2d ( 𝑥 = ( 𝑓𝑘 ) → ( ( 𝑅𝑘 ) ≤ ( 𝐹𝑥 ) ↔ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) )
59 1 56 58 axcc4 ( ∀ 𝑘 ∈ ℕ ∃ 𝑥𝑋 ( 𝑅𝑘 ) ≤ ( 𝐹𝑥 ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) )
60 55 59 syl ( 𝜑 → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) )
61 nnuz ℕ = ( ℤ ‘ 1 )
62 1zzd ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) → 1 ∈ ℤ )
63 1zzd ( 𝜑 → 1 ∈ ℤ )
64 23 recnd ( 𝜑𝑆 ∈ ℂ )
65 1z 1 ∈ ℤ
66 61 eqimss2i ( ℤ ‘ 1 ) ⊆ ℕ
67 nnex ℕ ∈ V
68 66 67 climconst2 ( ( 𝑆 ∈ ℂ ∧ 1 ∈ ℤ ) → ( ℕ × { 𝑆 } ) ⇝ 𝑆 )
69 64 65 68 sylancl ( 𝜑 → ( ℕ × { 𝑆 } ) ⇝ 𝑆 )
70 67 mptex ( 𝑛 ∈ ℕ ↦ ( 𝑆 − ( 1 / 𝑛 ) ) ) ∈ V
71 3 70 eqeltri 𝑅 ∈ V
72 71 a1i ( 𝜑𝑅 ∈ V )
73 ax-1cn 1 ∈ ℂ
74 divcnv ( 1 ∈ ℂ → ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ⇝ 0 )
75 73 74 mp1i ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ⇝ 0 )
76 fvconst2g ( ( 𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( ℕ × { 𝑆 } ) ‘ 𝑘 ) = 𝑆 )
77 23 76 sylan ( ( 𝜑𝑘 ∈ ℕ ) → ( ( ℕ × { 𝑆 } ) ‘ 𝑘 ) = 𝑆 )
78 64 adantr ( ( 𝜑𝑘 ∈ ℕ ) → 𝑆 ∈ ℂ )
79 77 78 eqeltrd ( ( 𝜑𝑘 ∈ ℕ ) → ( ( ℕ × { 𝑆 } ) ‘ 𝑘 ) ∈ ℂ )
80 eqid ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) )
81 ovex ( 1 / 𝑘 ) ∈ V
82 8 80 81 fvmpt ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ‘ 𝑘 ) = ( 1 / 𝑘 ) )
83 82 adantl ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ‘ 𝑘 ) = ( 1 / 𝑘 ) )
84 nnrecre ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ )
85 84 recnd ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℂ )
86 85 adantl ( ( 𝜑𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ∈ ℂ )
87 83 86 eqeltrd ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ‘ 𝑘 ) ∈ ℂ )
88 77 83 oveq12d ( ( 𝜑𝑘 ∈ ℕ ) → ( ( ( ℕ × { 𝑆 } ) ‘ 𝑘 ) − ( ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ‘ 𝑘 ) ) = ( 𝑆 − ( 1 / 𝑘 ) ) )
89 12 88 eqtr4d ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑅𝑘 ) = ( ( ( ℕ × { 𝑆 } ) ‘ 𝑘 ) − ( ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ‘ 𝑘 ) ) )
90 61 63 69 72 75 79 87 89 climsub ( 𝜑𝑅 ⇝ ( 𝑆 − 0 ) )
91 64 subid1d ( 𝜑 → ( 𝑆 − 0 ) = 𝑆 )
92 90 91 breqtrd ( 𝜑𝑅𝑆 )
93 92 ad2antrr ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) → 𝑅𝑆 )
94 14 ad2antrr ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) → 𝐹 : 𝑋𝐴 )
95 fex ( ( 𝐹 : 𝑋𝐴𝑋 ∈ V ) → 𝐹 ∈ V )
96 94 1 95 sylancl ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) → 𝐹 ∈ V )
97 vex 𝑓 ∈ V
98 coexg ( ( 𝐹 ∈ V ∧ 𝑓 ∈ V ) → ( 𝐹𝑓 ) ∈ V )
99 96 97 98 sylancl ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) → ( 𝐹𝑓 ) ∈ V )
100 34 ad2antrr ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) → 𝑅 : ℕ ⟶ ℝ )
101 100 ffvelrnda ( ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝑅𝑚 ) ∈ ℝ )
102 14 6 fssd ( 𝜑𝐹 : 𝑋 ⟶ ℝ )
103 fco ( ( 𝐹 : 𝑋 ⟶ ℝ ∧ 𝑓 : ℕ ⟶ 𝑋 ) → ( 𝐹𝑓 ) : ℕ ⟶ ℝ )
104 102 103 sylan ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) → ( 𝐹𝑓 ) : ℕ ⟶ ℝ )
105 104 adantr ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) → ( 𝐹𝑓 ) : ℕ ⟶ ℝ )
106 105 ffvelrnda ( ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝐹𝑓 ) ‘ 𝑚 ) ∈ ℝ )
107 fveq2 ( 𝑘 = 𝑚 → ( 𝑅𝑘 ) = ( 𝑅𝑚 ) )
108 2fveq3 ( 𝑘 = 𝑚 → ( 𝐹 ‘ ( 𝑓𝑘 ) ) = ( 𝐹 ‘ ( 𝑓𝑚 ) ) )
109 107 108 breq12d ( 𝑘 = 𝑚 → ( ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ↔ ( 𝑅𝑚 ) ≤ ( 𝐹 ‘ ( 𝑓𝑚 ) ) ) )
110 109 rspccva ( ( ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝑅𝑚 ) ≤ ( 𝐹 ‘ ( 𝑓𝑚 ) ) )
111 110 adantll ( ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝑅𝑚 ) ≤ ( 𝐹 ‘ ( 𝑓𝑚 ) ) )
112 simplr ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) → 𝑓 : ℕ ⟶ 𝑋 )
113 fvco3 ( ( 𝑓 : ℕ ⟶ 𝑋𝑚 ∈ ℕ ) → ( ( 𝐹𝑓 ) ‘ 𝑚 ) = ( 𝐹 ‘ ( 𝑓𝑚 ) ) )
114 112 113 sylan ( ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝐹𝑓 ) ‘ 𝑚 ) = ( 𝐹 ‘ ( 𝑓𝑚 ) ) )
115 111 114 breqtrrd ( ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝑅𝑚 ) ≤ ( ( 𝐹𝑓 ) ‘ 𝑚 ) )
116 30 ad3antrrr ( ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ) )
117 112 ffvelrnda ( ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝑓𝑚 ) ∈ 𝑋 )
118 94 ffvelrnda ( ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) ∧ ( 𝑓𝑚 ) ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑓𝑚 ) ) ∈ 𝐴 )
119 117 118 syldan ( ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑓𝑚 ) ) ∈ 𝐴 )
120 suprub ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 ) ∧ ( 𝐹 ‘ ( 𝑓𝑚 ) ) ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝑓𝑚 ) ) ≤ sup ( 𝐴 , ℝ , < ) )
121 116 119 120 syl2anc ( ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑓𝑚 ) ) ≤ sup ( 𝐴 , ℝ , < ) )
122 121 2 breqtrrdi ( ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑓𝑚 ) ) ≤ 𝑆 )
123 114 122 eqbrtrd ( ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝐹𝑓 ) ‘ 𝑚 ) ≤ 𝑆 )
124 61 62 93 99 101 106 115 123 climsqz ( ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) → ( 𝐹𝑓 ) ⇝ 𝑆 )
125 124 ex ( ( 𝜑𝑓 : ℕ ⟶ 𝑋 ) → ( ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) → ( 𝐹𝑓 ) ⇝ 𝑆 ) )
126 125 imdistanda ( 𝜑 → ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) → ( 𝑓 : ℕ ⟶ 𝑋 ∧ ( 𝐹𝑓 ) ⇝ 𝑆 ) ) )
127 126 eximdv ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝑅𝑘 ) ≤ ( 𝐹 ‘ ( 𝑓𝑘 ) ) ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 ∧ ( 𝐹𝑓 ) ⇝ 𝑆 ) ) )
128 60 127 mpd ( 𝜑 → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 ∧ ( 𝐹𝑓 ) ⇝ 𝑆 ) )