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

Theorem supcvg 15202
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 9846. (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 7148 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘))
21oveq2d 7156 . . . . . . . . . . 11 (𝑛 = 𝑘 → (𝑆 − (1 / 𝑛)) = (𝑆 − (1 / 𝑘)))
3 supcvg.3 . . . . . . . . . . 11 𝑅 = (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛)))
4 ovex 7173 . . . . . . . . . . 11 (𝑆 − (1 / 𝑘)) ∈ V
52, 3, 4fvmpt 6750 . . . . . . . . . 10 (𝑘 ∈ ℕ → (𝑅𝑘) = (𝑆 − (1 / 𝑘)))
65adantl 485 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) = (𝑆 − (1 / 𝑘)))
7 supcvg.2 . . . . . . . . . . 11 𝑆 = sup(𝐴, ℝ, < )
8 supcvg.6 . . . . . . . . . . . 12 (𝜑𝐴 ⊆ ℝ)
9 supcvg.4 . . . . . . . . . . . . 13 (𝜑𝑋 ≠ ∅)
10 supcvg.5 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:𝑋onto𝐴)
11 fof 6572 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋onto𝐴𝐹:𝑋𝐴)
1210, 11syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑋𝐴)
13 feq3 6477 . . . . . . . . . . . . . . . 16 (𝐴 = ∅ → (𝐹:𝑋𝐴𝐹:𝑋⟶∅))
1412, 13syl5ibcom 248 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 = ∅ → 𝐹:𝑋⟶∅))
15 f00 6542 . . . . . . . . . . . . . . . 16 (𝐹:𝑋⟶∅ ↔ (𝐹 = ∅ ∧ 𝑋 = ∅))
1615simprbi 500 . . . . . . . . . . . . . . 15 (𝐹:𝑋⟶∅ → 𝑋 = ∅)
1714, 16syl6 35 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 = ∅ → 𝑋 = ∅))
1817necon3d 3032 . . . . . . . . . . . . 13 (𝜑 → (𝑋 ≠ ∅ → 𝐴 ≠ ∅))
199, 18mpd 15 . . . . . . . . . . . 12 (𝜑𝐴 ≠ ∅)
20 supcvg.7 . . . . . . . . . . . 12 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥)
218, 19, 20suprcld 11591 . . . . . . . . . . 11 (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
227, 21eqeltrid 2918 . . . . . . . . . 10 (𝜑𝑆 ∈ ℝ)
23 nnrp 12388 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
2423rpreccld 12429 . . . . . . . . . 10 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
25 ltsubrp 12413 . . . . . . . . . 10 ((𝑆 ∈ ℝ ∧ (1 / 𝑘) ∈ ℝ+) → (𝑆 − (1 / 𝑘)) < 𝑆)
2622, 24, 25syl2an 598 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝑆 − (1 / 𝑘)) < 𝑆)
276, 26eqbrtrd 5064 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) < 𝑆)
2827, 7breqtrdi 5083 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) < sup(𝐴, ℝ, < ))
298, 19, 203jca 1125 . . . . . . . 8 (𝜑 → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
30 nnrecre 11667 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
31 resubcl 10939 . . . . . . . . . . 11 ((𝑆 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ) → (𝑆 − (1 / 𝑛)) ∈ ℝ)
3222, 30, 31syl2an 598 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑆 − (1 / 𝑛)) ∈ ℝ)
3332, 3fmptd 6860 . . . . . . . . 9 (𝜑𝑅:ℕ⟶ℝ)
3433ffvelrnda 6833 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) ∈ ℝ)
35 suprlub 11592 . . . . . . . 8 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ (𝑅𝑘) ∈ ℝ) → ((𝑅𝑘) < sup(𝐴, ℝ, < ) ↔ ∃𝑧𝐴 (𝑅𝑘) < 𝑧))
3629, 34, 35syl2an2r 684 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((𝑅𝑘) < sup(𝐴, ℝ, < ) ↔ ∃𝑧𝐴 (𝑅𝑘) < 𝑧))
3728, 36mpbid 235 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ∃𝑧𝐴 (𝑅𝑘) < 𝑧)
388adantr 484 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 𝐴 ⊆ ℝ)
3938sselda 3942 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑧𝐴) → 𝑧 ∈ ℝ)
40 ltle 10718 . . . . . . . 8 (((𝑅𝑘) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑅𝑘) < 𝑧 → (𝑅𝑘) ≤ 𝑧))
4134, 39, 40syl2an2r 684 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑧𝐴) → ((𝑅𝑘) < 𝑧 → (𝑅𝑘) ≤ 𝑧))
4241reximdva 3260 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (∃𝑧𝐴 (𝑅𝑘) < 𝑧 → ∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧))
4337, 42mpd 15 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧)
44 forn 6575 . . . . . . . . 9 (𝐹:𝑋onto𝐴 → ran 𝐹 = 𝐴)
4510, 44syl 17 . . . . . . . 8 (𝜑 → ran 𝐹 = 𝐴)
4645rexeqdv 3393 . . . . . . 7 (𝜑 → (∃𝑧 ∈ ran 𝐹(𝑅𝑘) ≤ 𝑧 ↔ ∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧))
47 ffn 6494 . . . . . . . 8 (𝐹:𝑋𝐴𝐹 Fn 𝑋)
48 breq2 5046 . . . . . . . . 9 (𝑧 = (𝐹𝑥) → ((𝑅𝑘) ≤ 𝑧 ↔ (𝑅𝑘) ≤ (𝐹𝑥)))
4948rexrn 6835 . . . . . . . 8 (𝐹 Fn 𝑋 → (∃𝑧 ∈ ran 𝐹(𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5012, 47, 493syl 18 . . . . . . 7 (𝜑 → (∃𝑧 ∈ ran 𝐹(𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5146, 50bitr3d 284 . . . . . 6 (𝜑 → (∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5251adantr 484 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5343, 52mpbid 235 . . . 4 ((𝜑𝑘 ∈ ℕ) → ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥))
5453ralrimiva 3174 . . 3 (𝜑 → ∀𝑘 ∈ ℕ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥))
55 supcvg.1 . . . 4 𝑋 ∈ V
56 nnenom 13343 . . . 4 ℕ ≈ ω
57 fveq2 6652 . . . . 5 (𝑥 = (𝑓𝑘) → (𝐹𝑥) = (𝐹‘(𝑓𝑘)))
5857breq2d 5054 . . . 4 (𝑥 = (𝑓𝑘) → ((𝑅𝑘) ≤ (𝐹𝑥) ↔ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))))
5955, 56, 58axcc4 9850 . . 3 (∀𝑘 ∈ ℕ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))))
6054, 59syl 17 . 2 (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))))
61 nnuz 12269 . . . . . 6 ℕ = (ℤ‘1)
62 1zzd 12001 . . . . . 6 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 1 ∈ ℤ)
63 1zzd 12001 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
6422recnd 10658 . . . . . . . . . 10 (𝜑𝑆 ∈ ℂ)
65 1z 12000 . . . . . . . . . 10 1 ∈ ℤ
6661eqimss2i 4001 . . . . . . . . . . 11 (ℤ‘1) ⊆ ℕ
67 nnex 11631 . . . . . . . . . . 11 ℕ ∈ V
6866, 67climconst2 14896 . . . . . . . . . 10 ((𝑆 ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {𝑆}) ⇝ 𝑆)
6964, 65, 68sylancl 589 . . . . . . . . 9 (𝜑 → (ℕ × {𝑆}) ⇝ 𝑆)
7067mptex 6968 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛))) ∈ V
713, 70eqeltri 2910 . . . . . . . . . 10 𝑅 ∈ V
7271a1i 11 . . . . . . . . 9 (𝜑𝑅 ∈ V)
73 ax-1cn 10584 . . . . . . . . . 10 1 ∈ ℂ
74 divcnv 15199 . . . . . . . . . 10 (1 ∈ ℂ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
7573, 74mp1i 13 . . . . . . . . 9 (𝜑 → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
76 fvconst2g 6946 . . . . . . . . . . 11 ((𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ) → ((ℕ × {𝑆})‘𝑘) = 𝑆)
7722, 76sylan 583 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((ℕ × {𝑆})‘𝑘) = 𝑆)
7864adantr 484 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝑆 ∈ ℂ)
7977, 78eqeltrd 2914 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((ℕ × {𝑆})‘𝑘) ∈ ℂ)
80 eqid 2822 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ (1 / 𝑛)) = (𝑛 ∈ ℕ ↦ (1 / 𝑛))
81 ovex 7173 . . . . . . . . . . . 12 (1 / 𝑘) ∈ V
821, 80, 81fvmpt 6750 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) = (1 / 𝑘))
8382adantl 485 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) = (1 / 𝑘))
84 nnrecre 11667 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
8584recnd 10658 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℂ)
8685adantl 485 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (1 / 𝑘) ∈ ℂ)
8783, 86eqeltrd 2914 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) ∈ ℂ)
8877, 83oveq12d 7158 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (((ℕ × {𝑆})‘𝑘) − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)) = (𝑆 − (1 / 𝑘)))
896, 88eqtr4d 2860 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) = (((ℕ × {𝑆})‘𝑘) − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)))
9061, 63, 69, 72, 75, 79, 87, 89climsub 14981 . . . . . . . 8 (𝜑𝑅 ⇝ (𝑆 − 0))
9164subid1d 10975 . . . . . . . 8 (𝜑 → (𝑆 − 0) = 𝑆)
9290, 91breqtrd 5068 . . . . . . 7 (𝜑𝑅𝑆)
9392ad2antrr 725 . . . . . 6 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝑅𝑆)
9412ad2antrr 725 . . . . . . . 8 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝐹:𝑋𝐴)
95 fex 6971 . . . . . . . 8 ((𝐹:𝑋𝐴𝑋 ∈ V) → 𝐹 ∈ V)
9694, 55, 95sylancl 589 . . . . . . 7 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝐹 ∈ V)
97 vex 3472 . . . . . . 7 𝑓 ∈ V
98 coexg 7620 . . . . . . 7 ((𝐹 ∈ V ∧ 𝑓 ∈ V) → (𝐹𝑓) ∈ V)
9996, 97, 98sylancl 589 . . . . . 6 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝐹𝑓) ∈ V)
10033ad2antrr 725 . . . . . . 7 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝑅:ℕ⟶ℝ)
101100ffvelrnda 6833 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ∈ ℝ)
10212, 8fssd 6509 . . . . . . . . 9 (𝜑𝐹:𝑋⟶ℝ)
103 fco 6512 . . . . . . . . 9 ((𝐹:𝑋⟶ℝ ∧ 𝑓:ℕ⟶𝑋) → (𝐹𝑓):ℕ⟶ℝ)
104102, 103sylan 583 . . . . . . . 8 ((𝜑𝑓:ℕ⟶𝑋) → (𝐹𝑓):ℕ⟶ℝ)
105104adantr 484 . . . . . . 7 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝐹𝑓):ℕ⟶ℝ)
106105ffvelrnda 6833 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) ∈ ℝ)
107 fveq2 6652 . . . . . . . . . 10 (𝑘 = 𝑚 → (𝑅𝑘) = (𝑅𝑚))
108 2fveq3 6657 . . . . . . . . . 10 (𝑘 = 𝑚 → (𝐹‘(𝑓𝑘)) = (𝐹‘(𝑓𝑚)))
109107, 108breq12d 5055 . . . . . . . . 9 (𝑘 = 𝑚 → ((𝑅𝑘) ≤ (𝐹‘(𝑓𝑘)) ↔ (𝑅𝑚) ≤ (𝐹‘(𝑓𝑚))))
110109rspccva 3597 . . . . . . . 8 ((∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘)) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ≤ (𝐹‘(𝑓𝑚)))
111110adantll 713 . . . . . . 7 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ≤ (𝐹‘(𝑓𝑚)))
112 simplr 768 . . . . . . . 8 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝑓:ℕ⟶𝑋)
113 fvco3 6742 . . . . . . . 8 ((𝑓:ℕ⟶𝑋𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) = (𝐹‘(𝑓𝑚)))
114112, 113sylan 583 . . . . . . 7 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) = (𝐹‘(𝑓𝑚)))
115111, 114breqtrrd 5070 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ≤ ((𝐹𝑓)‘𝑚))
11629ad3antrrr 729 . . . . . . . . 9 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
117112ffvelrnda 6833 . . . . . . . . . 10 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑓𝑚) ∈ 𝑋)
11894ffvelrnda 6833 . . . . . . . . . 10 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ (𝑓𝑚) ∈ 𝑋) → (𝐹‘(𝑓𝑚)) ∈ 𝐴)
119117, 118syldan 594 . . . . . . . . 9 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓𝑚)) ∈ 𝐴)
120 suprub 11589 . . . . . . . . 9 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ (𝐹‘(𝑓𝑚)) ∈ 𝐴) → (𝐹‘(𝑓𝑚)) ≤ sup(𝐴, ℝ, < ))
121116, 119, 120syl2anc 587 . . . . . . . 8 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓𝑚)) ≤ sup(𝐴, ℝ, < ))
122121, 7breqtrrdi 5084 . . . . . . 7 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓𝑚)) ≤ 𝑆)
123114, 122eqbrtrd 5064 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) ≤ 𝑆)
12461, 62, 93, 99, 101, 106, 115, 123climsqz 14988 . . . . 5 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝐹𝑓) ⇝ 𝑆)
125124ex 416 . . . 4 ((𝜑𝑓:ℕ⟶𝑋) → (∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘)) → (𝐹𝑓) ⇝ 𝑆))
126125imdistanda 575 . . 3 (𝜑 → ((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝑓:ℕ⟶𝑋 ∧ (𝐹𝑓) ⇝ 𝑆)))
127126eximdv 1918 . 2 (𝜑 → (∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹𝑓) ⇝ 𝑆)))
12860, 127mpd 15 1 (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹𝑓) ⇝ 𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wex 1781  wcel 2114  wne 3011  wral 3130  wrex 3131  Vcvv 3469  wss 3908  c0 4265  {csn 4539   class class class wbr 5042  cmpt 5122   × cxp 5530  ran crn 5533  ccom 5536   Fn wfn 6329  wf 6330  ontowfo 6332  cfv 6334  (class class class)co 7140  supcsup 8892  cc 10524  cr 10525  0cc0 10526  1c1 10527   < clt 10664  cle 10665  cmin 10859   / cdiv 11286  cn 11625  cz 11969  cuz 12231  +crp 12377  cli 14832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-inf2 9092  ax-cc 9846  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-pm 8396  df-en 8497  df-dom 8498  df-sdom 8499  df-sup 8894  df-inf 8895  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-rp 12378  df-fl 13157  df-seq 13365  df-exp 13426  df-cj 14449  df-re 14450  df-im 14451  df-sqrt 14585  df-abs 14586  df-clim 14836  df-rlim 14837
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator