MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  supcvg Structured version   Visualization version   GIF version

Theorem supcvg 15892
Description: Extract a sequence 𝑓 in 𝑋 such that the image of the points in the bounded set 𝐴 converges to the supremum 𝑆 of the set. Similar to Equation 4 of [Kreyszig] p. 144. The proof uses countable choice ax-cc 10475. (Contributed by Mario Carneiro, 15-Feb-2013.) (Proof shortened by Mario Carneiro, 26-Apr-2014.)
Hypotheses
Ref Expression
supcvg.1 𝑋 ∈ V
supcvg.2 𝑆 = sup(𝐴, ℝ, < )
supcvg.3 𝑅 = (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛)))
supcvg.4 (𝜑𝑋 ≠ ∅)
supcvg.5 (𝜑𝐹:𝑋onto𝐴)
supcvg.6 (𝜑𝐴 ⊆ ℝ)
supcvg.7 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥)
Assertion
Ref Expression
supcvg (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹𝑓) ⇝ 𝑆))
Distinct variable groups:   𝑥,𝑓,𝐹   𝑓,𝑛,𝜑   𝑅,𝑓,𝑥   𝑓,𝑋,𝑥   𝑥,𝑦,𝐴   𝑆,𝑛
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑓,𝑛)   𝑅(𝑦,𝑛)   𝑆(𝑥,𝑦,𝑓)   𝐹(𝑦,𝑛)   𝑋(𝑦,𝑛)

Proof of Theorem supcvg
Dummy variables 𝑘 𝑚 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7439 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘))
21oveq2d 7447 . . . . . . . . . . 11 (𝑛 = 𝑘 → (𝑆 − (1 / 𝑛)) = (𝑆 − (1 / 𝑘)))
3 supcvg.3 . . . . . . . . . . 11 𝑅 = (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛)))
4 ovex 7464 . . . . . . . . . . 11 (𝑆 − (1 / 𝑘)) ∈ V
52, 3, 4fvmpt 7016 . . . . . . . . . 10 (𝑘 ∈ ℕ → (𝑅𝑘) = (𝑆 − (1 / 𝑘)))
65adantl 481 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) = (𝑆 − (1 / 𝑘)))
7 supcvg.2 . . . . . . . . . . 11 𝑆 = sup(𝐴, ℝ, < )
8 supcvg.6 . . . . . . . . . . . 12 (𝜑𝐴 ⊆ ℝ)
9 supcvg.4 . . . . . . . . . . . . 13 (𝜑𝑋 ≠ ∅)
10 supcvg.5 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:𝑋onto𝐴)
11 fof 6820 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋onto𝐴𝐹:𝑋𝐴)
1210, 11syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑋𝐴)
13 feq3 6718 . . . . . . . . . . . . . . . 16 (𝐴 = ∅ → (𝐹:𝑋𝐴𝐹:𝑋⟶∅))
1412, 13syl5ibcom 245 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 = ∅ → 𝐹:𝑋⟶∅))
15 f00 6790 . . . . . . . . . . . . . . . 16 (𝐹:𝑋⟶∅ ↔ (𝐹 = ∅ ∧ 𝑋 = ∅))
1615simprbi 496 . . . . . . . . . . . . . . 15 (𝐹:𝑋⟶∅ → 𝑋 = ∅)
1714, 16syl6 35 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 = ∅ → 𝑋 = ∅))
1817necon3d 2961 . . . . . . . . . . . . 13 (𝜑 → (𝑋 ≠ ∅ → 𝐴 ≠ ∅))
199, 18mpd 15 . . . . . . . . . . . 12 (𝜑𝐴 ≠ ∅)
20 supcvg.7 . . . . . . . . . . . 12 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥)
218, 19, 20suprcld 12231 . . . . . . . . . . 11 (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
227, 21eqeltrid 2845 . . . . . . . . . 10 (𝜑𝑆 ∈ ℝ)
23 nnrp 13046 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
2423rpreccld 13087 . . . . . . . . . 10 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
25 ltsubrp 13071 . . . . . . . . . 10 ((𝑆 ∈ ℝ ∧ (1 / 𝑘) ∈ ℝ+) → (𝑆 − (1 / 𝑘)) < 𝑆)
2622, 24, 25syl2an 596 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝑆 − (1 / 𝑘)) < 𝑆)
276, 26eqbrtrd 5165 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) < 𝑆)
2827, 7breqtrdi 5184 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) < sup(𝐴, ℝ, < ))
298, 19, 203jca 1129 . . . . . . . 8 (𝜑 → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
30 nnrecre 12308 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
31 resubcl 11573 . . . . . . . . . . 11 ((𝑆 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ) → (𝑆 − (1 / 𝑛)) ∈ ℝ)
3222, 30, 31syl2an 596 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑆 − (1 / 𝑛)) ∈ ℝ)
3332, 3fmptd 7134 . . . . . . . . 9 (𝜑𝑅:ℕ⟶ℝ)
3433ffvelcdmda 7104 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) ∈ ℝ)
35 suprlub 12232 . . . . . . . 8 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ (𝑅𝑘) ∈ ℝ) → ((𝑅𝑘) < sup(𝐴, ℝ, < ) ↔ ∃𝑧𝐴 (𝑅𝑘) < 𝑧))
3629, 34, 35syl2an2r 685 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((𝑅𝑘) < sup(𝐴, ℝ, < ) ↔ ∃𝑧𝐴 (𝑅𝑘) < 𝑧))
3728, 36mpbid 232 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ∃𝑧𝐴 (𝑅𝑘) < 𝑧)
388adantr 480 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 𝐴 ⊆ ℝ)
3938sselda 3983 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑧𝐴) → 𝑧 ∈ ℝ)
40 ltle 11349 . . . . . . . 8 (((𝑅𝑘) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑅𝑘) < 𝑧 → (𝑅𝑘) ≤ 𝑧))
4134, 39, 40syl2an2r 685 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑧𝐴) → ((𝑅𝑘) < 𝑧 → (𝑅𝑘) ≤ 𝑧))
4241reximdva 3168 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (∃𝑧𝐴 (𝑅𝑘) < 𝑧 → ∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧))
4337, 42mpd 15 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧)
44 forn 6823 . . . . . . . . 9 (𝐹:𝑋onto𝐴 → ran 𝐹 = 𝐴)
4510, 44syl 17 . . . . . . . 8 (𝜑 → ran 𝐹 = 𝐴)
4645rexeqdv 3327 . . . . . . 7 (𝜑 → (∃𝑧 ∈ ran 𝐹(𝑅𝑘) ≤ 𝑧 ↔ ∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧))
47 ffn 6736 . . . . . . . 8 (𝐹:𝑋𝐴𝐹 Fn 𝑋)
48 breq2 5147 . . . . . . . . 9 (𝑧 = (𝐹𝑥) → ((𝑅𝑘) ≤ 𝑧 ↔ (𝑅𝑘) ≤ (𝐹𝑥)))
4948rexrn 7107 . . . . . . . 8 (𝐹 Fn 𝑋 → (∃𝑧 ∈ ran 𝐹(𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5012, 47, 493syl 18 . . . . . . 7 (𝜑 → (∃𝑧 ∈ ran 𝐹(𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5146, 50bitr3d 281 . . . . . 6 (𝜑 → (∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5251adantr 480 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5343, 52mpbid 232 . . . 4 ((𝜑𝑘 ∈ ℕ) → ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥))
5453ralrimiva 3146 . . 3 (𝜑 → ∀𝑘 ∈ ℕ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥))
55 supcvg.1 . . . 4 𝑋 ∈ V
56 nnenom 14021 . . . 4 ℕ ≈ ω
57 fveq2 6906 . . . . 5 (𝑥 = (𝑓𝑘) → (𝐹𝑥) = (𝐹‘(𝑓𝑘)))
5857breq2d 5155 . . . 4 (𝑥 = (𝑓𝑘) → ((𝑅𝑘) ≤ (𝐹𝑥) ↔ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))))
5955, 56, 58axcc4 10479 . . 3 (∀𝑘 ∈ ℕ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))))
6054, 59syl 17 . 2 (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))))
61 nnuz 12921 . . . . . 6 ℕ = (ℤ‘1)
62 1zzd 12648 . . . . . 6 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 1 ∈ ℤ)
63 1zzd 12648 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
6422recnd 11289 . . . . . . . . . 10 (𝜑𝑆 ∈ ℂ)
65 1z 12647 . . . . . . . . . 10 1 ∈ ℤ
6661eqimss2i 4045 . . . . . . . . . . 11 (ℤ‘1) ⊆ ℕ
67 nnex 12272 . . . . . . . . . . 11 ℕ ∈ V
6866, 67climconst2 15584 . . . . . . . . . 10 ((𝑆 ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {𝑆}) ⇝ 𝑆)
6964, 65, 68sylancl 586 . . . . . . . . 9 (𝜑 → (ℕ × {𝑆}) ⇝ 𝑆)
7067mptex 7243 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛))) ∈ V
713, 70eqeltri 2837 . . . . . . . . . 10 𝑅 ∈ V
7271a1i 11 . . . . . . . . 9 (𝜑𝑅 ∈ V)
73 ax-1cn 11213 . . . . . . . . . 10 1 ∈ ℂ
74 divcnv 15889 . . . . . . . . . 10 (1 ∈ ℂ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
7573, 74mp1i 13 . . . . . . . . 9 (𝜑 → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
76 fvconst2g 7222 . . . . . . . . . . 11 ((𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ) → ((ℕ × {𝑆})‘𝑘) = 𝑆)
7722, 76sylan 580 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((ℕ × {𝑆})‘𝑘) = 𝑆)
7864adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝑆 ∈ ℂ)
7977, 78eqeltrd 2841 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((ℕ × {𝑆})‘𝑘) ∈ ℂ)
80 eqid 2737 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ (1 / 𝑛)) = (𝑛 ∈ ℕ ↦ (1 / 𝑛))
81 ovex 7464 . . . . . . . . . . . 12 (1 / 𝑘) ∈ V
821, 80, 81fvmpt 7016 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) = (1 / 𝑘))
8382adantl 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) = (1 / 𝑘))
84 nnrecre 12308 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
8584recnd 11289 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℂ)
8685adantl 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (1 / 𝑘) ∈ ℂ)
8783, 86eqeltrd 2841 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) ∈ ℂ)
8877, 83oveq12d 7449 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (((ℕ × {𝑆})‘𝑘) − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)) = (𝑆 − (1 / 𝑘)))
896, 88eqtr4d 2780 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) = (((ℕ × {𝑆})‘𝑘) − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)))
9061, 63, 69, 72, 75, 79, 87, 89climsub 15670 . . . . . . . 8 (𝜑𝑅 ⇝ (𝑆 − 0))
9164subid1d 11609 . . . . . . . 8 (𝜑 → (𝑆 − 0) = 𝑆)
9290, 91breqtrd 5169 . . . . . . 7 (𝜑𝑅𝑆)
9392ad2antrr 726 . . . . . 6 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝑅𝑆)
9412ad2antrr 726 . . . . . . . 8 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝐹:𝑋𝐴)
95 fex 7246 . . . . . . . 8 ((𝐹:𝑋𝐴𝑋 ∈ V) → 𝐹 ∈ V)
9694, 55, 95sylancl 586 . . . . . . 7 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝐹 ∈ V)
97 vex 3484 . . . . . . 7 𝑓 ∈ V
98 coexg 7951 . . . . . . 7 ((𝐹 ∈ V ∧ 𝑓 ∈ V) → (𝐹𝑓) ∈ V)
9996, 97, 98sylancl 586 . . . . . 6 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝐹𝑓) ∈ V)
10033ad2antrr 726 . . . . . . 7 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝑅:ℕ⟶ℝ)
101100ffvelcdmda 7104 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ∈ ℝ)
10212, 8fssd 6753 . . . . . . . . 9 (𝜑𝐹:𝑋⟶ℝ)
103 fco 6760 . . . . . . . . 9 ((𝐹:𝑋⟶ℝ ∧ 𝑓:ℕ⟶𝑋) → (𝐹𝑓):ℕ⟶ℝ)
104102, 103sylan 580 . . . . . . . 8 ((𝜑𝑓:ℕ⟶𝑋) → (𝐹𝑓):ℕ⟶ℝ)
105104adantr 480 . . . . . . 7 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝐹𝑓):ℕ⟶ℝ)
106105ffvelcdmda 7104 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) ∈ ℝ)
107 fveq2 6906 . . . . . . . . . 10 (𝑘 = 𝑚 → (𝑅𝑘) = (𝑅𝑚))
108 2fveq3 6911 . . . . . . . . . 10 (𝑘 = 𝑚 → (𝐹‘(𝑓𝑘)) = (𝐹‘(𝑓𝑚)))
109107, 108breq12d 5156 . . . . . . . . 9 (𝑘 = 𝑚 → ((𝑅𝑘) ≤ (𝐹‘(𝑓𝑘)) ↔ (𝑅𝑚) ≤ (𝐹‘(𝑓𝑚))))
110109rspccva 3621 . . . . . . . 8 ((∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘)) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ≤ (𝐹‘(𝑓𝑚)))
111110adantll 714 . . . . . . 7 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ≤ (𝐹‘(𝑓𝑚)))
112 simplr 769 . . . . . . . 8 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝑓:ℕ⟶𝑋)
113 fvco3 7008 . . . . . . . 8 ((𝑓:ℕ⟶𝑋𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) = (𝐹‘(𝑓𝑚)))
114112, 113sylan 580 . . . . . . 7 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) = (𝐹‘(𝑓𝑚)))
115111, 114breqtrrd 5171 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ≤ ((𝐹𝑓)‘𝑚))
11629ad3antrrr 730 . . . . . . . . 9 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
117112ffvelcdmda 7104 . . . . . . . . . 10 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑓𝑚) ∈ 𝑋)
11894ffvelcdmda 7104 . . . . . . . . . 10 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ (𝑓𝑚) ∈ 𝑋) → (𝐹‘(𝑓𝑚)) ∈ 𝐴)
119117, 118syldan 591 . . . . . . . . 9 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓𝑚)) ∈ 𝐴)
120 suprub 12229 . . . . . . . . 9 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ (𝐹‘(𝑓𝑚)) ∈ 𝐴) → (𝐹‘(𝑓𝑚)) ≤ sup(𝐴, ℝ, < ))
121116, 119, 120syl2anc 584 . . . . . . . 8 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓𝑚)) ≤ sup(𝐴, ℝ, < ))
122121, 7breqtrrdi 5185 . . . . . . 7 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓𝑚)) ≤ 𝑆)
123114, 122eqbrtrd 5165 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) ≤ 𝑆)
12461, 62, 93, 99, 101, 106, 115, 123climsqz 15677 . . . . 5 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝐹𝑓) ⇝ 𝑆)
125124ex 412 . . . 4 ((𝜑𝑓:ℕ⟶𝑋) → (∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘)) → (𝐹𝑓) ⇝ 𝑆))
126125imdistanda 571 . . 3 (𝜑 → ((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝑓:ℕ⟶𝑋 ∧ (𝐹𝑓) ⇝ 𝑆)))
127126eximdv 1917 . 2 (𝜑 → (∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹𝑓) ⇝ 𝑆)))
12860, 127mpd 15 1 (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹𝑓) ⇝ 𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wex 1779  wcel 2108  wne 2940  wral 3061  wrex 3070  Vcvv 3480  wss 3951  c0 4333  {csn 4626   class class class wbr 5143  cmpt 5225   × cxp 5683  ran crn 5686  ccom 5689   Fn wfn 6556  wf 6557  ontowfo 6559  cfv 6561  (class class class)co 7431  supcsup 9480  cc 11153  cr 11154  0cc0 11155  1c1 11156   < clt 11295  cle 11296  cmin 11492   / cdiv 11920  cn 12266  cz 12613  cuz 12878  +crp 13034  cli 15520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cc 10475  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-sup 9482  df-inf 9483  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-rp 13035  df-fl 13832  df-seq 14043  df-exp 14103  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-rlim 15525
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator