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

Theorem supcvg 15889
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 10473. (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 6821 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋onto𝐴𝐹:𝑋𝐴)
1210, 11syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑋𝐴)
13 feq3 6719 . . . . . . . . . . . . . . . 16 (𝐴 = ∅ → (𝐹:𝑋𝐴𝐹:𝑋⟶∅))
1412, 13syl5ibcom 245 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 = ∅ → 𝐹:𝑋⟶∅))
15 f00 6791 . . . . . . . . . . . . . . . 16 (𝐹:𝑋⟶∅ ↔ (𝐹 = ∅ ∧ 𝑋 = ∅))
1615simprbi 496 . . . . . . . . . . . . . . 15 (𝐹:𝑋⟶∅ → 𝑋 = ∅)
1714, 16syl6 35 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 = ∅ → 𝑋 = ∅))
1817necon3d 2959 . . . . . . . . . . . . 13 (𝜑 → (𝑋 ≠ ∅ → 𝐴 ≠ ∅))
199, 18mpd 15 . . . . . . . . . . . 12 (𝜑𝐴 ≠ ∅)
20 supcvg.7 . . . . . . . . . . . 12 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥)
218, 19, 20suprcld 12229 . . . . . . . . . . 11 (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
227, 21eqeltrid 2843 . . . . . . . . . 10 (𝜑𝑆 ∈ ℝ)
23 nnrp 13044 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
2423rpreccld 13085 . . . . . . . . . 10 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
25 ltsubrp 13069 . . . . . . . . . 10 ((𝑆 ∈ ℝ ∧ (1 / 𝑘) ∈ ℝ+) → (𝑆 − (1 / 𝑘)) < 𝑆)
2622, 24, 25syl2an 596 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝑆 − (1 / 𝑘)) < 𝑆)
276, 26eqbrtrd 5170 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) < 𝑆)
2827, 7breqtrdi 5189 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) < sup(𝐴, ℝ, < ))
298, 19, 203jca 1127 . . . . . . . 8 (𝜑 → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
30 nnrecre 12306 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
31 resubcl 11571 . . . . . . . . . . 11 ((𝑆 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ) → (𝑆 − (1 / 𝑛)) ∈ ℝ)
3222, 30, 31syl2an 596 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑆 − (1 / 𝑛)) ∈ ℝ)
3332, 3fmptd 7134 . . . . . . . . 9 (𝜑𝑅:ℕ⟶ℝ)
3433ffvelcdmda 7104 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) ∈ ℝ)
35 suprlub 12230 . . . . . . . 8 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ (𝑅𝑘) ∈ ℝ) → ((𝑅𝑘) < sup(𝐴, ℝ, < ) ↔ ∃𝑧𝐴 (𝑅𝑘) < 𝑧))
3629, 34, 35syl2an2r 685 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((𝑅𝑘) < sup(𝐴, ℝ, < ) ↔ ∃𝑧𝐴 (𝑅𝑘) < 𝑧))
3728, 36mpbid 232 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ∃𝑧𝐴 (𝑅𝑘) < 𝑧)
388adantr 480 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 𝐴 ⊆ ℝ)
3938sselda 3995 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑧𝐴) → 𝑧 ∈ ℝ)
40 ltle 11347 . . . . . . . 8 (((𝑅𝑘) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑅𝑘) < 𝑧 → (𝑅𝑘) ≤ 𝑧))
4134, 39, 40syl2an2r 685 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑧𝐴) → ((𝑅𝑘) < 𝑧 → (𝑅𝑘) ≤ 𝑧))
4241reximdva 3166 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (∃𝑧𝐴 (𝑅𝑘) < 𝑧 → ∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧))
4337, 42mpd 15 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧)
44 forn 6824 . . . . . . . . 9 (𝐹:𝑋onto𝐴 → ran 𝐹 = 𝐴)
4510, 44syl 17 . . . . . . . 8 (𝜑 → ran 𝐹 = 𝐴)
4645rexeqdv 3325 . . . . . . 7 (𝜑 → (∃𝑧 ∈ ran 𝐹(𝑅𝑘) ≤ 𝑧 ↔ ∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧))
47 ffn 6737 . . . . . . . 8 (𝐹:𝑋𝐴𝐹 Fn 𝑋)
48 breq2 5152 . . . . . . . . 9 (𝑧 = (𝐹𝑥) → ((𝑅𝑘) ≤ 𝑧 ↔ (𝑅𝑘) ≤ (𝐹𝑥)))
4948rexrn 7107 . . . . . . . 8 (𝐹 Fn 𝑋 → (∃𝑧 ∈ ran 𝐹(𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5012, 47, 493syl 18 . . . . . . 7 (𝜑 → (∃𝑧 ∈ ran 𝐹(𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5146, 50bitr3d 281 . . . . . 6 (𝜑 → (∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5251adantr 480 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5343, 52mpbid 232 . . . 4 ((𝜑𝑘 ∈ ℕ) → ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥))
5453ralrimiva 3144 . . 3 (𝜑 → ∀𝑘 ∈ ℕ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥))
55 supcvg.1 . . . 4 𝑋 ∈ V
56 nnenom 14018 . . . 4 ℕ ≈ ω
57 fveq2 6907 . . . . 5 (𝑥 = (𝑓𝑘) → (𝐹𝑥) = (𝐹‘(𝑓𝑘)))
5857breq2d 5160 . . . 4 (𝑥 = (𝑓𝑘) → ((𝑅𝑘) ≤ (𝐹𝑥) ↔ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))))
5955, 56, 58axcc4 10477 . . 3 (∀𝑘 ∈ ℕ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))))
6054, 59syl 17 . 2 (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))))
61 nnuz 12919 . . . . . 6 ℕ = (ℤ‘1)
62 1zzd 12646 . . . . . 6 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 1 ∈ ℤ)
63 1zzd 12646 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
6422recnd 11287 . . . . . . . . . 10 (𝜑𝑆 ∈ ℂ)
65 1z 12645 . . . . . . . . . 10 1 ∈ ℤ
6661eqimss2i 4057 . . . . . . . . . . 11 (ℤ‘1) ⊆ ℕ
67 nnex 12270 . . . . . . . . . . 11 ℕ ∈ V
6866, 67climconst2 15581 . . . . . . . . . 10 ((𝑆 ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {𝑆}) ⇝ 𝑆)
6964, 65, 68sylancl 586 . . . . . . . . 9 (𝜑 → (ℕ × {𝑆}) ⇝ 𝑆)
7067mptex 7243 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛))) ∈ V
713, 70eqeltri 2835 . . . . . . . . . 10 𝑅 ∈ V
7271a1i 11 . . . . . . . . 9 (𝜑𝑅 ∈ V)
73 ax-1cn 11211 . . . . . . . . . 10 1 ∈ ℂ
74 divcnv 15886 . . . . . . . . . 10 (1 ∈ ℂ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
7573, 74mp1i 13 . . . . . . . . 9 (𝜑 → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
76 fvconst2g 7222 . . . . . . . . . . 11 ((𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ) → ((ℕ × {𝑆})‘𝑘) = 𝑆)
7722, 76sylan 580 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((ℕ × {𝑆})‘𝑘) = 𝑆)
7864adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝑆 ∈ ℂ)
7977, 78eqeltrd 2839 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((ℕ × {𝑆})‘𝑘) ∈ ℂ)
80 eqid 2735 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ (1 / 𝑛)) = (𝑛 ∈ ℕ ↦ (1 / 𝑛))
81 ovex 7464 . . . . . . . . . . . 12 (1 / 𝑘) ∈ V
821, 80, 81fvmpt 7016 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) = (1 / 𝑘))
8382adantl 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) = (1 / 𝑘))
84 nnrecre 12306 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
8584recnd 11287 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℂ)
8685adantl 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (1 / 𝑘) ∈ ℂ)
8783, 86eqeltrd 2839 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) ∈ ℂ)
8877, 83oveq12d 7449 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (((ℕ × {𝑆})‘𝑘) − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)) = (𝑆 − (1 / 𝑘)))
896, 88eqtr4d 2778 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) = (((ℕ × {𝑆})‘𝑘) − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)))
9061, 63, 69, 72, 75, 79, 87, 89climsub 15667 . . . . . . . 8 (𝜑𝑅 ⇝ (𝑆 − 0))
9164subid1d 11607 . . . . . . . 8 (𝜑 → (𝑆 − 0) = 𝑆)
9290, 91breqtrd 5174 . . . . . . 7 (𝜑𝑅𝑆)
9392ad2antrr 726 . . . . . 6 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝑅𝑆)
9412ad2antrr 726 . . . . . . . 8 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝐹:𝑋𝐴)
95 fex 7246 . . . . . . . 8 ((𝐹:𝑋𝐴𝑋 ∈ V) → 𝐹 ∈ V)
9694, 55, 95sylancl 586 . . . . . . 7 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝐹 ∈ V)
97 vex 3482 . . . . . . 7 𝑓 ∈ V
98 coexg 7952 . . . . . . 7 ((𝐹 ∈ V ∧ 𝑓 ∈ V) → (𝐹𝑓) ∈ V)
9996, 97, 98sylancl 586 . . . . . 6 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝐹𝑓) ∈ V)
10033ad2antrr 726 . . . . . . 7 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝑅:ℕ⟶ℝ)
101100ffvelcdmda 7104 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ∈ ℝ)
10212, 8fssd 6754 . . . . . . . . 9 (𝜑𝐹:𝑋⟶ℝ)
103 fco 6761 . . . . . . . . 9 ((𝐹:𝑋⟶ℝ ∧ 𝑓:ℕ⟶𝑋) → (𝐹𝑓):ℕ⟶ℝ)
104102, 103sylan 580 . . . . . . . 8 ((𝜑𝑓:ℕ⟶𝑋) → (𝐹𝑓):ℕ⟶ℝ)
105104adantr 480 . . . . . . 7 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝐹𝑓):ℕ⟶ℝ)
106105ffvelcdmda 7104 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) ∈ ℝ)
107 fveq2 6907 . . . . . . . . . 10 (𝑘 = 𝑚 → (𝑅𝑘) = (𝑅𝑚))
108 2fveq3 6912 . . . . . . . . . 10 (𝑘 = 𝑚 → (𝐹‘(𝑓𝑘)) = (𝐹‘(𝑓𝑚)))
109107, 108breq12d 5161 . . . . . . . . 9 (𝑘 = 𝑚 → ((𝑅𝑘) ≤ (𝐹‘(𝑓𝑘)) ↔ (𝑅𝑚) ≤ (𝐹‘(𝑓𝑚))))
110109rspccva 3621 . . . . . . . 8 ((∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘)) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ≤ (𝐹‘(𝑓𝑚)))
111110adantll 714 . . . . . . 7 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ≤ (𝐹‘(𝑓𝑚)))
112 simplr 769 . . . . . . . 8 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝑓:ℕ⟶𝑋)
113 fvco3 7008 . . . . . . . 8 ((𝑓:ℕ⟶𝑋𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) = (𝐹‘(𝑓𝑚)))
114112, 113sylan 580 . . . . . . 7 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) = (𝐹‘(𝑓𝑚)))
115111, 114breqtrrd 5176 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ≤ ((𝐹𝑓)‘𝑚))
11629ad3antrrr 730 . . . . . . . . 9 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
117112ffvelcdmda 7104 . . . . . . . . . 10 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑓𝑚) ∈ 𝑋)
11894ffvelcdmda 7104 . . . . . . . . . 10 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ (𝑓𝑚) ∈ 𝑋) → (𝐹‘(𝑓𝑚)) ∈ 𝐴)
119117, 118syldan 591 . . . . . . . . 9 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓𝑚)) ∈ 𝐴)
120 suprub 12227 . . . . . . . . 9 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ (𝐹‘(𝑓𝑚)) ∈ 𝐴) → (𝐹‘(𝑓𝑚)) ≤ sup(𝐴, ℝ, < ))
121116, 119, 120syl2anc 584 . . . . . . . 8 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓𝑚)) ≤ sup(𝐴, ℝ, < ))
122121, 7breqtrrdi 5190 . . . . . . 7 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓𝑚)) ≤ 𝑆)
123114, 122eqbrtrd 5170 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) ≤ 𝑆)
12461, 62, 93, 99, 101, 106, 115, 123climsqz 15674 . . . . 5 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝐹𝑓) ⇝ 𝑆)
125124ex 412 . . . 4 ((𝜑𝑓:ℕ⟶𝑋) → (∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘)) → (𝐹𝑓) ⇝ 𝑆))
126125imdistanda 571 . . 3 (𝜑 → ((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝑓:ℕ⟶𝑋 ∧ (𝐹𝑓) ⇝ 𝑆)))
127126eximdv 1915 . 2 (𝜑 → (∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹𝑓) ⇝ 𝑆)))
12860, 127mpd 15 1 (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹𝑓) ⇝ 𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wex 1776  wcel 2106  wne 2938  wral 3059  wrex 3068  Vcvv 3478  wss 3963  c0 4339  {csn 4631   class class class wbr 5148  cmpt 5231   × cxp 5687  ran crn 5690  ccom 5693   Fn wfn 6558  wf 6559  ontowfo 6561  cfv 6563  (class class class)co 7431  supcsup 9478  cc 11151  cr 11152  0cc0 11153  1c1 11154   < clt 11293  cle 11294  cmin 11490   / cdiv 11918  cn 12264  cz 12611  cuz 12876  +crp 13032  cli 15517
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-inf2 9679  ax-cc 10473  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-er 8744  df-pm 8868  df-en 8985  df-dom 8986  df-sdom 8987  df-sup 9480  df-inf 9481  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-z 12612  df-uz 12877  df-rp 13033  df-fl 13829  df-seq 14040  df-exp 14100  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-clim 15521  df-rlim 15522
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator