Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  uzublem Structured version   Visualization version   GIF version

Theorem uzublem 43206
Description: A set of reals, indexed by upper integers, is bound if and only if any upper part is bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Hypotheses
Ref Expression
uzublem.1 𝑗𝜑
uzublem.2 𝑗𝑋
uzublem.3 (𝜑𝑀 ∈ ℤ)
uzublem.4 𝑍 = (ℤ𝑀)
uzublem.5 (𝜑𝑌 ∈ ℝ)
uzublem.6 𝑊 = sup(ran (𝑗 ∈ (𝑀...𝐾) ↦ 𝐵), ℝ, < )
uzublem.7 𝑋 = if(𝑊𝑌, 𝑌, 𝑊)
uzublem.8 (𝜑𝐾𝑍)
uzublem.9 ((𝜑𝑗𝑍) → 𝐵 ∈ ℝ)
uzublem.10 (𝜑 → ∀𝑗 ∈ (ℤ𝐾)𝐵𝑌)
Assertion
Ref Expression
uzublem (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗𝑍 𝐵𝑥)
Distinct variable groups:   𝑥,𝐵   𝑗,𝐾   𝑗,𝑀   𝑥,𝑋   𝑥,𝑍   𝑥,𝑗
Allowed substitution hints:   𝜑(𝑥,𝑗)   𝐵(𝑗)   𝐾(𝑥)   𝑀(𝑥)   𝑊(𝑥,𝑗)   𝑋(𝑗)   𝑌(𝑥,𝑗)   𝑍(𝑗)

Proof of Theorem uzublem
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 uzublem.7 . . 3 𝑋 = if(𝑊𝑌, 𝑌, 𝑊)
2 uzublem.5 . . . 4 (𝜑𝑌 ∈ ℝ)
3 uzublem.6 . . . . . 6 𝑊 = sup(ran (𝑗 ∈ (𝑀...𝐾) ↦ 𝐵), ℝ, < )
43a1i 11 . . . . 5 (𝜑𝑊 = sup(ran (𝑗 ∈ (𝑀...𝐾) ↦ 𝐵), ℝ, < ))
5 uzublem.1 . . . . . 6 𝑗𝜑
6 ltso 11128 . . . . . . 7 < Or ℝ
76a1i 11 . . . . . 6 (𝜑 → < Or ℝ)
8 fzfid 13766 . . . . . 6 (𝜑 → (𝑀...𝐾) ∈ Fin)
9 uzublem.3 . . . . . . . 8 (𝜑𝑀 ∈ ℤ)
10 uzublem.8 . . . . . . . . 9 (𝜑𝐾𝑍)
11 uzublem.4 . . . . . . . . . 10 𝑍 = (ℤ𝑀)
1211eluzelz2 43179 . . . . . . . . 9 (𝐾𝑍𝐾 ∈ ℤ)
1310, 12syl 17 . . . . . . . 8 (𝜑𝐾 ∈ ℤ)
149zred 12499 . . . . . . . . 9 (𝜑𝑀 ∈ ℝ)
1514leidd 11614 . . . . . . . 8 (𝜑𝑀𝑀)
1610, 11eleqtrdi 2848 . . . . . . . . 9 (𝜑𝐾 ∈ (ℤ𝑀))
17 eluzle 12668 . . . . . . . . 9 (𝐾 ∈ (ℤ𝑀) → 𝑀𝐾)
1816, 17syl 17 . . . . . . . 8 (𝜑𝑀𝐾)
199, 13, 9, 15, 18elfzd 13320 . . . . . . 7 (𝜑𝑀 ∈ (𝑀...𝐾))
2019ne0d 4280 . . . . . 6 (𝜑 → (𝑀...𝐾) ≠ ∅)
21 fzssuz 13370 . . . . . . . . 9 (𝑀...𝐾) ⊆ (ℤ𝑀)
2211eqcomi 2746 . . . . . . . . 9 (ℤ𝑀) = 𝑍
2321, 22sseqtri 3967 . . . . . . . 8 (𝑀...𝐾) ⊆ 𝑍
24 id 22 . . . . . . . 8 (𝑗 ∈ (𝑀...𝐾) → 𝑗 ∈ (𝑀...𝐾))
2523, 24sselid 3929 . . . . . . 7 (𝑗 ∈ (𝑀...𝐾) → 𝑗𝑍)
26 uzublem.9 . . . . . . 7 ((𝜑𝑗𝑍) → 𝐵 ∈ ℝ)
2725, 26sylan2 593 . . . . . 6 ((𝜑𝑗 ∈ (𝑀...𝐾)) → 𝐵 ∈ ℝ)
285, 7, 8, 20, 27fisupclrnmpt 43174 . . . . 5 (𝜑 → sup(ran (𝑗 ∈ (𝑀...𝐾) ↦ 𝐵), ℝ, < ) ∈ ℝ)
294, 28eqeltrd 2838 . . . 4 (𝜑𝑊 ∈ ℝ)
302, 29ifcld 4517 . . 3 (𝜑 → if(𝑊𝑌, 𝑌, 𝑊) ∈ ℝ)
311, 30eqeltrid 2842 . 2 (𝜑𝑋 ∈ ℝ)
3226adantr 481 . . . . . 6 (((𝜑𝑗𝑍) ∧ 𝐾𝑗) → 𝐵 ∈ ℝ)
332ad2antrr 723 . . . . . 6 (((𝜑𝑗𝑍) ∧ 𝐾𝑗) → 𝑌 ∈ ℝ)
3431ad2antrr 723 . . . . . 6 (((𝜑𝑗𝑍) ∧ 𝐾𝑗) → 𝑋 ∈ ℝ)
35 uzublem.10 . . . . . . . 8 (𝜑 → ∀𝑗 ∈ (ℤ𝐾)𝐵𝑌)
3635ad2antrr 723 . . . . . . 7 (((𝜑𝑗𝑍) ∧ 𝐾𝑗) → ∀𝑗 ∈ (ℤ𝐾)𝐵𝑌)
37 eqid 2737 . . . . . . . 8 (ℤ𝐾) = (ℤ𝐾)
3813ad2antrr 723 . . . . . . . 8 (((𝜑𝑗𝑍) ∧ 𝐾𝑗) → 𝐾 ∈ ℤ)
3911eluzelz2 43179 . . . . . . . . 9 (𝑗𝑍𝑗 ∈ ℤ)
4039ad2antlr 724 . . . . . . . 8 (((𝜑𝑗𝑍) ∧ 𝐾𝑗) → 𝑗 ∈ ℤ)
41 simpr 485 . . . . . . . 8 (((𝜑𝑗𝑍) ∧ 𝐾𝑗) → 𝐾𝑗)
4237, 38, 40, 41eluzd 43185 . . . . . . 7 (((𝜑𝑗𝑍) ∧ 𝐾𝑗) → 𝑗 ∈ (ℤ𝐾))
43 rspa 3228 . . . . . . 7 ((∀𝑗 ∈ (ℤ𝐾)𝐵𝑌𝑗 ∈ (ℤ𝐾)) → 𝐵𝑌)
4436, 42, 43syl2anc 584 . . . . . 6 (((𝜑𝑗𝑍) ∧ 𝐾𝑗) → 𝐵𝑌)
45 max2 12994 . . . . . . . . 9 ((𝑊 ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑌 ≤ if(𝑊𝑌, 𝑌, 𝑊))
4629, 2, 45syl2anc 584 . . . . . . . 8 (𝜑𝑌 ≤ if(𝑊𝑌, 𝑌, 𝑊))
4746, 1breqtrrdi 5129 . . . . . . 7 (𝜑𝑌𝑋)
4847ad2antrr 723 . . . . . 6 (((𝜑𝑗𝑍) ∧ 𝐾𝑗) → 𝑌𝑋)
4932, 33, 34, 44, 48letrd 11205 . . . . 5 (((𝜑𝑗𝑍) ∧ 𝐾𝑗) → 𝐵𝑋)
50 simpr 485 . . . . . . 7 (((𝜑𝑗𝑍) ∧ ¬ 𝐾𝑗) → ¬ 𝐾𝑗)
51 uzssre 12677 . . . . . . . . . . 11 (ℤ𝑀) ⊆ ℝ
5211, 51eqsstri 3965 . . . . . . . . . 10 𝑍 ⊆ ℝ
5352sseli 3927 . . . . . . . . 9 (𝑗𝑍𝑗 ∈ ℝ)
5453ad2antlr 724 . . . . . . . 8 (((𝜑𝑗𝑍) ∧ ¬ 𝐾𝑗) → 𝑗 ∈ ℝ)
5552, 10sselid 3929 . . . . . . . . 9 (𝜑𝐾 ∈ ℝ)
5655ad2antrr 723 . . . . . . . 8 (((𝜑𝑗𝑍) ∧ ¬ 𝐾𝑗) → 𝐾 ∈ ℝ)
5754, 56ltnled 11195 . . . . . . 7 (((𝜑𝑗𝑍) ∧ ¬ 𝐾𝑗) → (𝑗 < 𝐾 ↔ ¬ 𝐾𝑗))
5850, 57mpbird 256 . . . . . 6 (((𝜑𝑗𝑍) ∧ ¬ 𝐾𝑗) → 𝑗 < 𝐾)
5926adantr 481 . . . . . . 7 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝐵 ∈ ℝ)
603, 29eqeltrrid 2843 . . . . . . . . 9 (𝜑 → sup(ran (𝑗 ∈ (𝑀...𝐾) ↦ 𝐵), ℝ, < ) ∈ ℝ)
613, 60eqeltrid 2842 . . . . . . . 8 (𝜑𝑊 ∈ ℝ)
6261ad2antrr 723 . . . . . . 7 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝑊 ∈ ℝ)
632, 61ifcld 4517 . . . . . . . . 9 (𝜑 → if(𝑊𝑌, 𝑌, 𝑊) ∈ ℝ)
641, 63eqeltrid 2842 . . . . . . . 8 (𝜑𝑋 ∈ ℝ)
6564ad2antrr 723 . . . . . . 7 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝑋 ∈ ℝ)
66 simpll 764 . . . . . . . . 9 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝜑)
679ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝑀 ∈ ℤ)
6813ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝐾 ∈ ℤ)
6911eleq2i 2829 . . . . . . . . . . . . . 14 (𝑗𝑍𝑗 ∈ (ℤ𝑀))
7069biimpi 215 . . . . . . . . . . . . 13 (𝑗𝑍𝑗 ∈ (ℤ𝑀))
7170ad2antlr 724 . . . . . . . . . . . 12 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝑗 ∈ (ℤ𝑀))
72 simpr 485 . . . . . . . . . . . 12 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝑗 < 𝐾)
7371, 68, 72elfzod 43176 . . . . . . . . . . 11 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝑗 ∈ (𝑀..^𝐾))
74 elfzouz 13464 . . . . . . . . . . . 12 (𝑗 ∈ (𝑀..^𝐾) → 𝑗 ∈ (ℤ𝑀))
7574, 22eleqtrdi 2848 . . . . . . . . . . 11 (𝑗 ∈ (𝑀..^𝐾) → 𝑗𝑍)
7673, 75, 393syl 18 . . . . . . . . . 10 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝑗 ∈ ℤ)
77 eluzle 12668 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) → 𝑀𝑗)
7870, 77syl 17 . . . . . . . . . . 11 (𝑗𝑍𝑀𝑗)
7978ad2antlr 724 . . . . . . . . . 10 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝑀𝑗)
8073, 75, 533syl 18 . . . . . . . . . . 11 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝑗 ∈ ℝ)
8155ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝐾 ∈ ℝ)
8280, 81, 72ltled 11196 . . . . . . . . . 10 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝑗𝐾)
8367, 68, 76, 79, 82elfzd 13320 . . . . . . . . 9 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝑗 ∈ (𝑀...𝐾))
845, 27ralrimia 3238 . . . . . . . . . . 11 (𝜑 → ∀𝑗 ∈ (𝑀...𝐾)𝐵 ∈ ℝ)
85 fimaxre3 11994 . . . . . . . . . . 11 (((𝑀...𝐾) ∈ Fin ∧ ∀𝑗 ∈ (𝑀...𝐾)𝐵 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑗 ∈ (𝑀...𝐾)𝐵𝑦)
868, 84, 85syl2anc 584 . . . . . . . . . 10 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑗 ∈ (𝑀...𝐾)𝐵𝑦)
875, 27, 86suprubrnmpt 43028 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑀...𝐾)) → 𝐵 ≤ sup(ran (𝑗 ∈ (𝑀...𝐾) ↦ 𝐵), ℝ, < ))
8866, 83, 87syl2anc 584 . . . . . . . 8 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝐵 ≤ sup(ran (𝑗 ∈ (𝑀...𝐾) ↦ 𝐵), ℝ, < ))
8988, 3breqtrrdi 5129 . . . . . . 7 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝐵𝑊)
90 max1 12992 . . . . . . . . . 10 ((𝑊 ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑊 ≤ if(𝑊𝑌, 𝑌, 𝑊))
9129, 2, 90syl2anc 584 . . . . . . . . 9 (𝜑𝑊 ≤ if(𝑊𝑌, 𝑌, 𝑊))
9291, 1breqtrrdi 5129 . . . . . . . 8 (𝜑𝑊𝑋)
9392ad2antrr 723 . . . . . . 7 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝑊𝑋)
9459, 62, 65, 89, 93letrd 11205 . . . . . 6 (((𝜑𝑗𝑍) ∧ 𝑗 < 𝐾) → 𝐵𝑋)
9558, 94syldan 591 . . . . 5 (((𝜑𝑗𝑍) ∧ ¬ 𝐾𝑗) → 𝐵𝑋)
9649, 95pm2.61dan 810 . . . 4 ((𝜑𝑗𝑍) → 𝐵𝑋)
9796ex 413 . . 3 (𝜑 → (𝑗𝑍𝐵𝑋))
985, 97ralrimi 3237 . 2 (𝜑 → ∀𝑗𝑍 𝐵𝑋)
99 nfv 1916 . . 3 𝑥𝑗𝑍 𝐵𝑋
100 nfcv 2905 . . . . 5 𝑗𝑥
101 uzublem.2 . . . . 5 𝑗𝑋
102100, 101nfeq 2918 . . . 4 𝑗 𝑥 = 𝑋
103 breq2 5091 . . . 4 (𝑥 = 𝑋 → (𝐵𝑥𝐵𝑋))
104102, 103ralbid 3253 . . 3 (𝑥 = 𝑋 → (∀𝑗𝑍 𝐵𝑥 ↔ ∀𝑗𝑍 𝐵𝑋))
10599, 104rspce 3559 . 2 ((𝑋 ∈ ℝ ∧ ∀𝑗𝑍 𝐵𝑋) → ∃𝑥 ∈ ℝ ∀𝑗𝑍 𝐵𝑥)
10631, 98, 105syl2anc 584 1 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗𝑍 𝐵𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1540  wnf 1784  wcel 2105  wnfc 2885  wral 3062  wrex 3071  ifcif 4471   class class class wbr 5087  cmpt 5170   Or wor 5520  ran crn 5608  cfv 6465  (class class class)co 7315  Fincfn 8781  supcsup 9269  cr 10943   < clt 11082  cle 11083  cz 12392  cuz 12655  ...cfz 13312  ..^cfzo 13455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-cnex 11000  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-addrcl 11005  ax-mulcl 11006  ax-mulrcl 11007  ax-mulcom 11008  ax-addass 11009  ax-mulass 11010  ax-distr 11011  ax-i2m1 11012  ax-1ne0 11013  ax-1rid 11014  ax-rnegex 11015  ax-rrecex 11016  ax-cnre 11017  ax-pre-lttri 11018  ax-pre-lttrn 11019  ax-pre-ltadd 11020  ax-pre-mulgt0 11021  ax-pre-sup 11022
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-riota 7272  df-ov 7318  df-oprab 7319  df-mpo 7320  df-om 7758  df-1st 7876  df-2nd 7877  df-frecs 8144  df-wrecs 8175  df-recs 8249  df-rdg 8288  df-1o 8344  df-er 8546  df-en 8782  df-dom 8783  df-sdom 8784  df-fin 8785  df-sup 9271  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088  df-sub 11280  df-neg 11281  df-nn 12047  df-n0 12307  df-z 12393  df-uz 12656  df-fz 13313  df-fzo 13456
This theorem is referenced by:  uzub  43207
  Copyright terms: Public domain W3C validator