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

Theorem supcvg 15071
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 9655. (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 6984 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘))
21oveq2d 6992 . . . . . . . . . . 11 (𝑛 = 𝑘 → (𝑆 − (1 / 𝑛)) = (𝑆 − (1 / 𝑘)))
3 supcvg.3 . . . . . . . . . . 11 𝑅 = (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛)))
4 ovex 7008 . . . . . . . . . . 11 (𝑆 − (1 / 𝑘)) ∈ V
52, 3, 4fvmpt 6595 . . . . . . . . . 10 (𝑘 ∈ ℕ → (𝑅𝑘) = (𝑆 − (1 / 𝑘)))
65adantl 474 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) = (𝑆 − (1 / 𝑘)))
7 supcvg.2 . . . . . . . . . . 11 𝑆 = sup(𝐴, ℝ, < )
8 supcvg.6 . . . . . . . . . . . 12 (𝜑𝐴 ⊆ ℝ)
9 supcvg.4 . . . . . . . . . . . . 13 (𝜑𝑋 ≠ ∅)
10 supcvg.5 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:𝑋onto𝐴)
11 fof 6419 . . . . . . . . . . . . . . . . 17 (𝐹:𝑋onto𝐴𝐹:𝑋𝐴)
1210, 11syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑋𝐴)
13 feq3 6327 . . . . . . . . . . . . . . . 16 (𝐴 = ∅ → (𝐹:𝑋𝐴𝐹:𝑋⟶∅))
1412, 13syl5ibcom 237 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 = ∅ → 𝐹:𝑋⟶∅))
15 f00 6390 . . . . . . . . . . . . . . . 16 (𝐹:𝑋⟶∅ ↔ (𝐹 = ∅ ∧ 𝑋 = ∅))
1615simprbi 489 . . . . . . . . . . . . . . 15 (𝐹:𝑋⟶∅ → 𝑋 = ∅)
1714, 16syl6 35 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 = ∅ → 𝑋 = ∅))
1817necon3d 2988 . . . . . . . . . . . . 13 (𝜑 → (𝑋 ≠ ∅ → 𝐴 ≠ ∅))
199, 18mpd 15 . . . . . . . . . . . 12 (𝜑𝐴 ≠ ∅)
20 supcvg.7 . . . . . . . . . . . 12 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥)
218, 19, 20suprcld 11405 . . . . . . . . . . 11 (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
227, 21syl5eqel 2870 . . . . . . . . . 10 (𝜑𝑆 ∈ ℝ)
23 nnrp 12217 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
2423rpreccld 12258 . . . . . . . . . 10 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
25 ltsubrp 12242 . . . . . . . . . 10 ((𝑆 ∈ ℝ ∧ (1 / 𝑘) ∈ ℝ+) → (𝑆 − (1 / 𝑘)) < 𝑆)
2622, 24, 25syl2an 586 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝑆 − (1 / 𝑘)) < 𝑆)
276, 26eqbrtrd 4951 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) < 𝑆)
2827, 7syl6breq 4970 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) < sup(𝐴, ℝ, < ))
298, 19, 203jca 1108 . . . . . . . 8 (𝜑 → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
30 nnrecre 11482 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
31 resubcl 10751 . . . . . . . . . . 11 ((𝑆 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ) → (𝑆 − (1 / 𝑛)) ∈ ℝ)
3222, 30, 31syl2an 586 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑆 − (1 / 𝑛)) ∈ ℝ)
3332, 3fmptd 6701 . . . . . . . . 9 (𝜑𝑅:ℕ⟶ℝ)
3433ffvelrnda 6676 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) ∈ ℝ)
35 suprlub 11406 . . . . . . . 8 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ (𝑅𝑘) ∈ ℝ) → ((𝑅𝑘) < sup(𝐴, ℝ, < ) ↔ ∃𝑧𝐴 (𝑅𝑘) < 𝑧))
3629, 34, 35syl2an2r 672 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((𝑅𝑘) < sup(𝐴, ℝ, < ) ↔ ∃𝑧𝐴 (𝑅𝑘) < 𝑧))
3728, 36mpbid 224 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ∃𝑧𝐴 (𝑅𝑘) < 𝑧)
388adantr 473 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 𝐴 ⊆ ℝ)
3938sselda 3858 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑧𝐴) → 𝑧 ∈ ℝ)
40 ltle 10529 . . . . . . . 8 (((𝑅𝑘) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑅𝑘) < 𝑧 → (𝑅𝑘) ≤ 𝑧))
4134, 39, 40syl2an2r 672 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑧𝐴) → ((𝑅𝑘) < 𝑧 → (𝑅𝑘) ≤ 𝑧))
4241reximdva 3219 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (∃𝑧𝐴 (𝑅𝑘) < 𝑧 → ∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧))
4337, 42mpd 15 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧)
44 forn 6422 . . . . . . . . 9 (𝐹:𝑋onto𝐴 → ran 𝐹 = 𝐴)
4510, 44syl 17 . . . . . . . 8 (𝜑 → ran 𝐹 = 𝐴)
4645rexeqdv 3356 . . . . . . 7 (𝜑 → (∃𝑧 ∈ ran 𝐹(𝑅𝑘) ≤ 𝑧 ↔ ∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧))
47 ffn 6344 . . . . . . . 8 (𝐹:𝑋𝐴𝐹 Fn 𝑋)
48 breq2 4933 . . . . . . . . 9 (𝑧 = (𝐹𝑥) → ((𝑅𝑘) ≤ 𝑧 ↔ (𝑅𝑘) ≤ (𝐹𝑥)))
4948rexrn 6678 . . . . . . . 8 (𝐹 Fn 𝑋 → (∃𝑧 ∈ ran 𝐹(𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5012, 47, 493syl 18 . . . . . . 7 (𝜑 → (∃𝑧 ∈ ran 𝐹(𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5146, 50bitr3d 273 . . . . . 6 (𝜑 → (∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5251adantr 473 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (∃𝑧𝐴 (𝑅𝑘) ≤ 𝑧 ↔ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥)))
5343, 52mpbid 224 . . . 4 ((𝜑𝑘 ∈ ℕ) → ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥))
5453ralrimiva 3132 . . 3 (𝜑 → ∀𝑘 ∈ ℕ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥))
55 supcvg.1 . . . 4 𝑋 ∈ V
56 nnenom 13163 . . . 4 ℕ ≈ ω
57 fveq2 6499 . . . . 5 (𝑥 = (𝑓𝑘) → (𝐹𝑥) = (𝐹‘(𝑓𝑘)))
5857breq2d 4941 . . . 4 (𝑥 = (𝑓𝑘) → ((𝑅𝑘) ≤ (𝐹𝑥) ↔ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))))
5955, 56, 58axcc4 9659 . . 3 (∀𝑘 ∈ ℕ ∃𝑥𝑋 (𝑅𝑘) ≤ (𝐹𝑥) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))))
6054, 59syl 17 . 2 (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))))
61 nnuz 12095 . . . . . 6 ℕ = (ℤ‘1)
62 1zzd 11826 . . . . . 6 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 1 ∈ ℤ)
63 1zzd 11826 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
6422recnd 10468 . . . . . . . . . 10 (𝜑𝑆 ∈ ℂ)
65 1z 11825 . . . . . . . . . 10 1 ∈ ℤ
6661eqimss2i 3916 . . . . . . . . . . 11 (ℤ‘1) ⊆ ℕ
67 nnex 11446 . . . . . . . . . . 11 ℕ ∈ V
6866, 67climconst2 14766 . . . . . . . . . 10 ((𝑆 ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {𝑆}) ⇝ 𝑆)
6964, 65, 68sylancl 577 . . . . . . . . 9 (𝜑 → (ℕ × {𝑆}) ⇝ 𝑆)
7067mptex 6812 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛))) ∈ V
713, 70eqeltri 2862 . . . . . . . . . 10 𝑅 ∈ V
7271a1i 11 . . . . . . . . 9 (𝜑𝑅 ∈ V)
73 ax-1cn 10393 . . . . . . . . . 10 1 ∈ ℂ
74 divcnv 15068 . . . . . . . . . 10 (1 ∈ ℂ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
7573, 74mp1i 13 . . . . . . . . 9 (𝜑 → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
76 fvconst2g 6791 . . . . . . . . . . 11 ((𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ) → ((ℕ × {𝑆})‘𝑘) = 𝑆)
7722, 76sylan 572 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((ℕ × {𝑆})‘𝑘) = 𝑆)
7864adantr 473 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝑆 ∈ ℂ)
7977, 78eqeltrd 2866 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((ℕ × {𝑆})‘𝑘) ∈ ℂ)
80 eqid 2778 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ (1 / 𝑛)) = (𝑛 ∈ ℕ ↦ (1 / 𝑛))
81 ovex 7008 . . . . . . . . . . . 12 (1 / 𝑘) ∈ V
821, 80, 81fvmpt 6595 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) = (1 / 𝑘))
8382adantl 474 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) = (1 / 𝑘))
84 nnrecre 11482 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
8584recnd 10468 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℂ)
8685adantl 474 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (1 / 𝑘) ∈ ℂ)
8783, 86eqeltrd 2866 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) ∈ ℂ)
8877, 83oveq12d 6994 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (((ℕ × {𝑆})‘𝑘) − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)) = (𝑆 − (1 / 𝑘)))
896, 88eqtr4d 2817 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝑅𝑘) = (((ℕ × {𝑆})‘𝑘) − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)))
9061, 63, 69, 72, 75, 79, 87, 89climsub 14851 . . . . . . . 8 (𝜑𝑅 ⇝ (𝑆 − 0))
9164subid1d 10787 . . . . . . . 8 (𝜑 → (𝑆 − 0) = 𝑆)
9290, 91breqtrd 4955 . . . . . . 7 (𝜑𝑅𝑆)
9392ad2antrr 713 . . . . . 6 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝑅𝑆)
9412ad2antrr 713 . . . . . . . 8 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝐹:𝑋𝐴)
95 fex 6815 . . . . . . . 8 ((𝐹:𝑋𝐴𝑋 ∈ V) → 𝐹 ∈ V)
9694, 55, 95sylancl 577 . . . . . . 7 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝐹 ∈ V)
97 vex 3418 . . . . . . 7 𝑓 ∈ V
98 coexg 7449 . . . . . . 7 ((𝐹 ∈ V ∧ 𝑓 ∈ V) → (𝐹𝑓) ∈ V)
9996, 97, 98sylancl 577 . . . . . 6 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝐹𝑓) ∈ V)
10033ad2antrr 713 . . . . . . 7 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝑅:ℕ⟶ℝ)
101100ffvelrnda 6676 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ∈ ℝ)
10212, 8fssd 6358 . . . . . . . . 9 (𝜑𝐹:𝑋⟶ℝ)
103 fco 6361 . . . . . . . . 9 ((𝐹:𝑋⟶ℝ ∧ 𝑓:ℕ⟶𝑋) → (𝐹𝑓):ℕ⟶ℝ)
104102, 103sylan 572 . . . . . . . 8 ((𝜑𝑓:ℕ⟶𝑋) → (𝐹𝑓):ℕ⟶ℝ)
105104adantr 473 . . . . . . 7 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝐹𝑓):ℕ⟶ℝ)
106105ffvelrnda 6676 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) ∈ ℝ)
107 fveq2 6499 . . . . . . . . . 10 (𝑘 = 𝑚 → (𝑅𝑘) = (𝑅𝑚))
108 2fveq3 6504 . . . . . . . . . 10 (𝑘 = 𝑚 → (𝐹‘(𝑓𝑘)) = (𝐹‘(𝑓𝑚)))
109107, 108breq12d 4942 . . . . . . . . 9 (𝑘 = 𝑚 → ((𝑅𝑘) ≤ (𝐹‘(𝑓𝑘)) ↔ (𝑅𝑚) ≤ (𝐹‘(𝑓𝑚))))
110109rspccva 3534 . . . . . . . 8 ((∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘)) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ≤ (𝐹‘(𝑓𝑚)))
111110adantll 701 . . . . . . 7 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ≤ (𝐹‘(𝑓𝑚)))
112 simplr 756 . . . . . . . 8 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → 𝑓:ℕ⟶𝑋)
113 fvco3 6588 . . . . . . . 8 ((𝑓:ℕ⟶𝑋𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) = (𝐹‘(𝑓𝑚)))
114112, 113sylan 572 . . . . . . 7 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) = (𝐹‘(𝑓𝑚)))
115111, 114breqtrrd 4957 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅𝑚) ≤ ((𝐹𝑓)‘𝑚))
11629ad3antrrr 717 . . . . . . . . 9 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
117112ffvelrnda 6676 . . . . . . . . . 10 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑓𝑚) ∈ 𝑋)
11894ffvelrnda 6676 . . . . . . . . . 10 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ (𝑓𝑚) ∈ 𝑋) → (𝐹‘(𝑓𝑚)) ∈ 𝐴)
119117, 118syldan 582 . . . . . . . . 9 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓𝑚)) ∈ 𝐴)
120 suprub 11403 . . . . . . . . 9 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ (𝐹‘(𝑓𝑚)) ∈ 𝐴) → (𝐹‘(𝑓𝑚)) ≤ sup(𝐴, ℝ, < ))
121116, 119, 120syl2anc 576 . . . . . . . 8 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓𝑚)) ≤ sup(𝐴, ℝ, < ))
122121, 7syl6breqr 4971 . . . . . . 7 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓𝑚)) ≤ 𝑆)
123114, 122eqbrtrd 4951 . . . . . 6 ((((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹𝑓)‘𝑚) ≤ 𝑆)
12461, 62, 93, 99, 101, 106, 115, 123climsqz 14858 . . . . 5 (((𝜑𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝐹𝑓) ⇝ 𝑆)
125124ex 405 . . . 4 ((𝜑𝑓:ℕ⟶𝑋) → (∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘)) → (𝐹𝑓) ⇝ 𝑆))
126125imdistanda 564 . . 3 (𝜑 → ((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → (𝑓:ℕ⟶𝑋 ∧ (𝐹𝑓) ⇝ 𝑆)))
127126eximdv 1876 . 2 (𝜑 → (∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅𝑘) ≤ (𝐹‘(𝑓𝑘))) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹𝑓) ⇝ 𝑆)))
12860, 127mpd 15 1 (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹𝑓) ⇝ 𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wex 1742  wcel 2050  wne 2967  wral 3088  wrex 3089  Vcvv 3415  wss 3829  c0 4178  {csn 4441   class class class wbr 4929  cmpt 5008   × cxp 5405  ran crn 5408  ccom 5411   Fn wfn 6183  wf 6184  ontowfo 6186  cfv 6188  (class class class)co 6976  supcsup 8699  cc 10333  cr 10334  0cc0 10335  1c1 10336   < clt 10474  cle 10475  cmin 10670   / cdiv 11098  cn 11439  cz 11793  cuz 12058  +crp 12204  cli 14702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-inf2 8898  ax-cc 9655  ax-cnex 10391  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411  ax-pre-mulgt0 10412  ax-pre-sup 10413
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-om 7397  df-2nd 7502  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-er 8089  df-pm 8209  df-en 8307  df-dom 8308  df-sdom 8309  df-sup 8701  df-inf 8702  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480  df-sub 10672  df-neg 10673  df-div 11099  df-nn 11440  df-2 11503  df-3 11504  df-n0 11708  df-z 11794  df-uz 12059  df-rp 12205  df-fl 12977  df-seq 13185  df-exp 13245  df-cj 14319  df-re 14320  df-im 14321  df-sqrt 14455  df-abs 14456  df-clim 14706  df-rlim 14707
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator