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

Theorem supcvg 14829
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 9551. (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 6891 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘))
21oveq2d 6899 . . . . . . . . . . 11 (𝑛 = 𝑘 → (𝑆 − (1 / 𝑛)) = (𝑆 − (1 / 𝑘)))
3 supcvg.3 . . . . . . . . . . 11 𝑅 = (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛)))
4 ovex 6915 . . . . . . . . . . 11 (𝑆 − (1 / 𝑘)) ∈ V
52, 3, 4fvmpt 6512 . . . . . . . . . 10 (𝑘 ∈ ℕ → (𝑅𝑘) = (𝑆 − (1 / 𝑘)))
65adantl 469 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) = (𝑆 − (1 / 𝑘)))
7 supcvg.2 . . . . . . . . . . 11 𝑆 = sup(𝐴, ℝ, < )
8 supcvg.6 . . . . . . . . . . . . 13 (𝜑𝐴 ⊆ ℝ)
9 supcvg.4 . . . . . . . . . . . . . 14 (𝜑𝑋 ≠ ∅)
10 supcvg.5 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:𝑋onto𝐴)
11 fof 6340 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑋onto𝐴𝐹:𝑋𝐴)
1210, 11syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:𝑋𝐴)
13 feq3 6248 . . . . . . . . . . . . . . . . 17 (𝐴 = ∅ → (𝐹:𝑋𝐴𝐹:𝑋⟶∅))
1412, 13syl5ibcom 236 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 = ∅ → 𝐹:𝑋⟶∅))
15 f00 6311 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋⟶∅ ↔ (𝐹 = ∅ ∧ 𝑋 = ∅))
1615simprbi 486 . . . . . . . . . . . . . . . 16 (𝐹:𝑋⟶∅ → 𝑋 = ∅)
1714, 16syl6 35 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 = ∅ → 𝑋 = ∅))
1817necon3d 3010 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 ≠ ∅ → 𝐴 ≠ ∅))
199, 18mpd 15 . . . . . . . . . . . . 13 (𝜑𝐴 ≠ ∅)
20 supcvg.7 . . . . . . . . . . . . 13 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥)
218, 19, 203jca 1151 . . . . . . . . . . . 12 (𝜑 → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
22 suprcl 11277 . . . . . . . . . . . 12 ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) → sup(𝐴, ℝ, < ) ∈ ℝ)
2321, 22syl 17 . . . . . . . . . . 11 (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
247, 23syl5eqel 2900 . . . . . . . . . 10 (𝜑𝑆 ∈ ℝ)
25 nnrp 12075 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
2625rpreccld 12115 . . . . . . . . . 10 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
27 ltsubrp 12099 . . . . . . . . . 10 ((𝑆 ∈ ℝ ∧ (1 / 𝑘) ∈ ℝ+) → (𝑆 − (1 / 𝑘)) < 𝑆)
2824, 26, 27syl2an 585 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝑆 − (1 / 𝑘)) < 𝑆)
296, 28eqbrtrd 4877 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) < 𝑆)
3029, 7syl6breq 4896 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) < sup(𝐴, ℝ, < ))
3121adantr 468 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
32 nnrecre 11354 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
33 resubcl 10639 . . . . . . . . . . 11 ((𝑆 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ) → (𝑆 − (1 / 𝑛)) ∈ ℝ)
3424, 32, 33syl2an 585 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑆 − (1 / 𝑛)) ∈ ℝ)
3534, 3fmptd 6615 . . . . . . . . 9 (𝜑𝑅:ℕ⟶ℝ)
3635ffvelrnda 6590 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) ∈ ℝ)
37 suprlub 11281 . . . . . . . 8 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ (𝑅𝑘) ∈ ℝ) → ((𝑅𝑘) < sup(𝐴, ℝ, < ) ↔ ∃𝑧𝐴 (𝑅𝑘) < 𝑧))
3831, 36, 37syl2anc 575 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((𝑅𝑘) < sup(𝐴, ℝ, < ) ↔ ∃𝑧𝐴 (𝑅𝑘) < 𝑧))
3930, 38mpbid 223 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ∃𝑧𝐴 (𝑅𝑘) < 𝑧)
4036adantr 468 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑧𝐴) → (𝑅𝑘) ∈ ℝ)
418adantr 468 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 𝐴 ⊆ ℝ)
4241sselda 3809 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑧𝐴) → 𝑧 ∈ ℝ)
43 ltle 10420 . . . . . . . 8 (((𝑅𝑘) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑅𝑘) < 𝑧 → (𝑅𝑘) ≤ 𝑧))
4440, 42, 43syl2anc 575 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑧𝐴) → ((𝑅𝑘) < 𝑧 → (𝑅𝑘) ≤ 𝑧))
4544reximdva 3215 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (∃𝑧𝐴 (𝑅𝑘) < 𝑧 → ∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧))
4639, 45mpd 15 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧)
47 forn 6343 . . . . . . . . 9 (𝐹:𝑋onto𝐴 → ran 𝐹 = 𝐴)
4810, 47syl 17 . . . . . . . 8 (𝜑 → ran 𝐹 = 𝐴)
4948rexeqdv 3345 . . . . . . 7 (𝜑 → (∃𝑧 ∈ ran 𝐹(𝑅𝑘) ≤ 𝑧 ↔ ∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧))
50 ffn 6265 . . . . . . . 8 (𝐹:𝑋𝐴𝐹 Fn 𝑋)
51 breq2 4859 . . . . . . . . 9 (𝑧 = (𝐹𝑥) → ((𝑅𝑘) ≤ 𝑧 ↔ (𝑅𝑘) ≤ (𝐹𝑥)))
5251rexrn 6592 . . . . . . . 8 (𝐹 Fn 𝑋 → (∃𝑧 ∈ ran 𝐹(𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5312, 50, 523syl 18 . . . . . . 7 (𝜑 → (∃𝑧 ∈ ran 𝐹(𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5449, 53bitr3d 272 . . . . . 6 (𝜑 → (∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5554adantr 468 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5646, 55mpbid 223 . . . 4 ((𝜑𝑘 ∈ ℕ) → ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥))
5756ralrimiva 3165 . . 3 (𝜑 → ∀𝑘 ∈ ℕ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥))
58 supcvg.1 . . . 4 𝑋 ∈ V
59 nnenom 13022 . . . 4 ℕ ≈ ω
60 fveq2 6417 . . . . 5 (𝑥 = (𝑓𝑘) → (𝐹𝑥) = (𝐹‘(𝑓𝑘)))
6160breq2d 4867 . . . 4 (𝑥 = (𝑓𝑘) → ((𝑅𝑘) ≤ (𝐹𝑥) ↔ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))))
6258, 59, 61axcc4 9555 . . 3 (∀𝑘 ∈ ℕ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))))
6357, 62syl 17 . 2 (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))))
64 nnuz 11960 . . . . . 6 ℕ = (ℤ‘1)
65 1zzd 11693 . . . . . 6 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 1 ∈ ℤ)
66 1zzd 11693 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
6724recnd 10362 . . . . . . . . . 10 (𝜑𝑆 ∈ ℂ)
68 1z 11692 . . . . . . . . . 10 1 ∈ ℤ
6964eqimss2i 3868 . . . . . . . . . . 11 (ℤ‘1) ⊆ ℕ
70 nnex 11321 . . . . . . . . . . 11 ℕ ∈ V
7169, 70climconst2 14521 . . . . . . . . . 10 ((𝑆 ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {𝑆}) ⇝ 𝑆)
7267, 68, 71sylancl 576 . . . . . . . . 9 (𝜑 → (ℕ × {𝑆}) ⇝ 𝑆)
7370mptex 6720 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛))) ∈ V
743, 73eqeltri 2892 . . . . . . . . . 10 𝑅 ∈ V
7574a1i 11 . . . . . . . . 9 (𝜑𝑅 ∈ V)
76 ax-1cn 10288 . . . . . . . . . 10 1 ∈ ℂ
77 divcnv 14826 . . . . . . . . . 10 (1 ∈ ℂ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
7876, 77mp1i 13 . . . . . . . . 9 (𝜑 → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
79 fvconst2g 6701 . . . . . . . . . . 11 ((𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ) → ((ℕ × {𝑆})‘𝑘) = 𝑆)
8024, 79sylan 571 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((ℕ × {𝑆})‘𝑘) = 𝑆)
8167adantr 468 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝑆 ∈ ℂ)
8280, 81eqeltrd 2896 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((ℕ × {𝑆})‘𝑘) ∈ ℂ)
83 eqid 2817 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ (1 / 𝑛)) = (𝑛 ∈ ℕ ↦ (1 / 𝑛))
84 ovex 6915 . . . . . . . . . . . 12 (1 / 𝑘) ∈ V
851, 83, 84fvmpt 6512 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) = (1 / 𝑘))
8685adantl 469 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) = (1 / 𝑘))
87 nnrecre 11354 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
8887recnd 10362 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℂ)
8988adantl 469 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (1 / 𝑘) ∈ ℂ)
9086, 89eqeltrd 2896 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) ∈ ℂ)
9180, 86oveq12d 6901 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (((ℕ × {𝑆})‘𝑘) − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)) = (𝑆 − (1 / 𝑘)))
926, 91eqtr4d 2854 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) = (((ℕ × {𝑆})‘𝑘) − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)))
9364, 66, 72, 75, 78, 82, 90, 92climsub 14606 . . . . . . . 8 (𝜑𝑅 ⇝ (𝑆 − 0))
9467subid1d 10675 . . . . . . . 8 (𝜑 → (𝑆 − 0) = 𝑆)
9593, 94breqtrd 4881 . . . . . . 7 (𝜑𝑅𝑆)
9695ad2antrr 708 . . . . . 6 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝑅𝑆)
9712ad2antrr 708 . . . . . . . 8 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝐹:𝑋𝐴)
98 fex 6723 . . . . . . . 8 ((𝐹:𝑋𝐴𝑋 ∈ V) → 𝐹 ∈ V)
9997, 58, 98sylancl 576 . . . . . . 7 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝐹 ∈ V)
100 vex 3405 . . . . . . 7 𝑓 ∈ V
101 coexg 7356 . . . . . . 7 ((𝐹 ∈ V ∧ 𝑓 ∈ V) → (𝐹𝑓) ∈ V)
10299, 100, 101sylancl 576 . . . . . 6 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝐹𝑓) ∈ V)
10335ad2antrr 708 . . . . . . 7 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝑅:ℕ⟶ℝ)
104103ffvelrnda 6590 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ∈ ℝ)
10512, 8fssd 6279 . . . . . . . . 9 (𝜑𝐹:𝑋⟶ℝ)
106 fco 6282 . . . . . . . . 9 ((𝐹:𝑋⟶ℝ ∧ 𝑓:ℕ⟶𝑋) → (𝐹𝑓):ℕ⟶ℝ)
107105, 106sylan 571 . . . . . . . 8 ((𝜑𝑓:ℕ⟶𝑋) → (𝐹𝑓):ℕ⟶ℝ)
108107adantr 468 . . . . . . 7 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝐹𝑓):ℕ⟶ℝ)
109108ffvelrnda 6590 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) ∈ ℝ)
110 fveq2 6417 . . . . . . . . . 10 (𝑘 = 𝑚 → (𝑅𝑘) = (𝑅𝑚))
111 2fveq3 6422 . . . . . . . . . 10 (𝑘 = 𝑚 → (𝐹‘(𝑓𝑘)) = (𝐹‘(𝑓𝑚)))
112110, 111breq12d 4868 . . . . . . . . 9 (𝑘 = 𝑚 → ((𝑅𝑘) ≤ (𝐹‘(𝑓𝑘)) ↔ (𝑅𝑚) ≤ (𝐹‘(𝑓𝑚))))
113112rspccva 3512 . . . . . . . 8 ((∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘)) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ≤ (𝐹‘(𝑓𝑚)))
114113adantll 696 . . . . . . 7 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ≤ (𝐹‘(𝑓𝑚)))
115 simplr 776 . . . . . . . 8 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝑓:ℕ⟶𝑋)
116 fvco3 6505 . . . . . . . 8 ((𝑓:ℕ⟶𝑋𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) = (𝐹‘(𝑓𝑚)))
117115, 116sylan 571 . . . . . . 7 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) = (𝐹‘(𝑓𝑚)))
118114, 117breqtrrd 4883 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ≤ ((𝐹𝑓)‘𝑚))
11921ad3antrrr 712 . . . . . . . . 9 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
120115ffvelrnda 6590 . . . . . . . . . 10 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑓𝑚) ∈ 𝑋)
12197ffvelrnda 6590 . . . . . . . . . 10 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ (𝑓𝑚) ∈ 𝑋) → (𝐹‘(𝑓𝑚)) ∈ 𝐴)
122120, 121syldan 581 . . . . . . . . 9 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓𝑚)) ∈ 𝐴)
123 suprub 11278 . . . . . . . . 9 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ (𝐹‘(𝑓𝑚)) ∈ 𝐴) → (𝐹‘(𝑓𝑚)) ≤ sup(𝐴, ℝ, < ))
124119, 122, 123syl2anc 575 . . . . . . . 8 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓𝑚)) ≤ sup(𝐴, ℝ, < ))
125124, 7syl6breqr 4897 . . . . . . 7 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓𝑚)) ≤ 𝑆)
126117, 125eqbrtrd 4877 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) ≤ 𝑆)
12764, 65, 96, 102, 104, 109, 118, 126climsqz 14613 . . . . 5 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝐹𝑓) ⇝ 𝑆)
128127ex 399 . . . 4 ((𝜑𝑓:ℕ⟶𝑋) → (∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘)) → (𝐹𝑓) ⇝ 𝑆))
129128imdistanda 563 . . 3 (𝜑 → ((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝑓:ℕ⟶𝑋 ∧ (𝐹𝑓) ⇝ 𝑆)))
130129eximdv 2008 . 2 (𝜑 → (∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹𝑓) ⇝ 𝑆)))
13163, 130mpd 15 1 (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹𝑓) ⇝ 𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wex 1859  wcel 2157  wne 2989  wral 3107  wrex 3108  Vcvv 3402  wss 3780  c0 4127  {csn 4381   class class class wbr 4855  cmpt 4934   × cxp 5322  ran crn 5325  ccom 5328   Fn wfn 6105  wf 6106  ontowfo 6108  cfv 6110  (class class class)co 6883  supcsup 8594  cc 10228  cr 10229  0cc0 10230  1c1 10231   < clt 10368  cle 10369  cmin 10560   / cdiv 10978  cn 11314  cz 11662  cuz 11923  +crp 12065  cli 14457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7188  ax-inf2 8794  ax-cc 9551  ax-cnex 10286  ax-resscn 10287  ax-1cn 10288  ax-icn 10289  ax-addcl 10290  ax-addrcl 10291  ax-mulcl 10292  ax-mulrcl 10293  ax-mulcom 10294  ax-addass 10295  ax-mulass 10296  ax-distr 10297  ax-i2m1 10298  ax-1ne0 10299  ax-1rid 10300  ax-rnegex 10301  ax-rrecex 10302  ax-cnre 10303  ax-pre-lttri 10304  ax-pre-lttrn 10305  ax-pre-ltadd 10306  ax-pre-mulgt0 10307  ax-pre-sup 10308
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5906  df-ord 5952  df-on 5953  df-lim 5954  df-suc 5955  df-iota 6073  df-fun 6112  df-fn 6113  df-f 6114  df-f1 6115  df-fo 6116  df-f1o 6117  df-fv 6118  df-riota 6844  df-ov 6886  df-oprab 6887  df-mpt2 6888  df-om 7305  df-2nd 7408  df-wrecs 7651  df-recs 7713  df-rdg 7751  df-er 7988  df-pm 8104  df-en 8202  df-dom 8203  df-sdom 8204  df-sup 8596  df-inf 8597  df-pnf 10370  df-mnf 10371  df-xr 10372  df-ltxr 10373  df-le 10374  df-sub 10562  df-neg 10563  df-div 10979  df-nn 11315  df-2 11375  df-3 11376  df-n0 11579  df-z 11663  df-uz 11924  df-rp 12066  df-fl 12836  df-seq 13044  df-exp 13103  df-cj 14081  df-re 14082  df-im 14083  df-sqrt 14217  df-abs 14218  df-clim 14461  df-rlim 14462
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator