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 ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 ∧ ( 𝐹 ∘ 𝑓 ) ⇝ 𝑆 ) )