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

Theorem pimincfltioc 43763
 Description: Given a nondecreasing function, the preimage of an unbounded below, open interval, when the supremum of the preimage belongs to the preimage. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypotheses
Ref Expression
pimincfltioc.x 𝑥𝜑
pimincfltioc.h 𝑦𝜑
pimincfltioc.a (𝜑𝐴 ⊆ ℝ)
pimincfltioc.f (𝜑𝐹:𝐴⟶ℝ*)
pimincfltioc.i (𝜑 → ∀𝑥𝐴𝑦𝐴 (𝑥𝑦 → (𝐹𝑥) ≤ (𝐹𝑦)))
pimincfltioc.r (𝜑𝑅 ∈ ℝ*)
pimincfltioc.y 𝑌 = {𝑥𝐴 ∣ (𝐹𝑥) < 𝑅}
pimincfltioc.c 𝑆 = sup(𝑌, ℝ*, < )
pimincfltioc.e (𝜑𝑆𝑌)
pimincfltioc.d 𝐼 = (-∞(,]𝑆)
Assertion
Ref Expression
pimincfltioc (𝜑𝑌 = (𝐼𝐴))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐹,𝑦   𝑥,𝐼,𝑦   𝑥,𝑅   𝑥,𝑆,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑅(𝑦)   𝑌(𝑥,𝑦)

Proof of Theorem pimincfltioc
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 pimincfltioc.y . . . . . . 7 𝑌 = {𝑥𝐴 ∣ (𝐹𝑥) < 𝑅}
2 ssrab2 3987 . . . . . . 7 {𝑥𝐴 ∣ (𝐹𝑥) < 𝑅} ⊆ 𝐴
31, 2eqsstri 3929 . . . . . 6 𝑌𝐴
43a1i 11 . . . . 5 (𝜑𝑌𝐴)
5 pimincfltioc.a . . . . 5 (𝜑𝐴 ⊆ ℝ)
64, 5sstrd 3905 . . . 4 (𝜑𝑌 ⊆ ℝ)
7 pimincfltioc.c . . . 4 𝑆 = sup(𝑌, ℝ*, < )
8 pimincfltioc.e . . . 4 (𝜑𝑆𝑌)
9 pimincfltioc.d . . . 4 𝐼 = (-∞(,]𝑆)
106, 7, 8, 9ressiocsup 42603 . . 3 (𝜑𝑌𝐼)
1110, 4ssind 4140 . 2 (𝜑𝑌 ⊆ (𝐼𝐴))
12 pimincfltioc.x . . . 4 𝑥𝜑
13 elinel2 4104 . . . . . . . 8 (𝑥 ∈ (𝐼𝐴) → 𝑥𝐴)
1413adantl 485 . . . . . . 7 ((𝜑𝑥 ∈ (𝐼𝐴)) → 𝑥𝐴)
15 pimincfltioc.f . . . . . . . . . 10 (𝜑𝐹:𝐴⟶ℝ*)
1615adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐼𝐴)) → 𝐹:𝐴⟶ℝ*)
1716, 14ffvelrnd 6850 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐼𝐴)) → (𝐹𝑥) ∈ ℝ*)
183, 8sseldi 3893 . . . . . . . . . 10 (𝜑𝑆𝐴)
1915, 18ffvelrnd 6850 . . . . . . . . 9 (𝜑 → (𝐹𝑆) ∈ ℝ*)
2019adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐼𝐴)) → (𝐹𝑆) ∈ ℝ*)
21 pimincfltioc.r . . . . . . . . 9 (𝜑𝑅 ∈ ℝ*)
2221adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐼𝐴)) → 𝑅 ∈ ℝ*)
23 eleq1w 2835 . . . . . . . . . . 11 (𝑧 = 𝑥 → (𝑧 ∈ (𝐼𝐴) ↔ 𝑥 ∈ (𝐼𝐴)))
2423anbi2d 631 . . . . . . . . . 10 (𝑧 = 𝑥 → ((𝜑𝑧 ∈ (𝐼𝐴)) ↔ (𝜑𝑥 ∈ (𝐼𝐴))))
25 fveq2 6664 . . . . . . . . . . 11 (𝑧 = 𝑥 → (𝐹𝑧) = (𝐹𝑥))
2625breq1d 5047 . . . . . . . . . 10 (𝑧 = 𝑥 → ((𝐹𝑧) ≤ (𝐹𝑆) ↔ (𝐹𝑥) ≤ (𝐹𝑆)))
2724, 26imbi12d 348 . . . . . . . . 9 (𝑧 = 𝑥 → (((𝜑𝑧 ∈ (𝐼𝐴)) → (𝐹𝑧) ≤ (𝐹𝑆)) ↔ ((𝜑𝑥 ∈ (𝐼𝐴)) → (𝐹𝑥) ≤ (𝐹𝑆))))
28 nfv 1916 . . . . . . . . . . 11 𝑥 𝑧 ∈ (𝐼𝐴)
2912, 28nfan 1901 . . . . . . . . . 10 𝑥(𝜑𝑧 ∈ (𝐼𝐴))
30 pimincfltioc.h . . . . . . . . . . 11 𝑦𝜑
31 nfv 1916 . . . . . . . . . . 11 𝑦 𝑧 ∈ (𝐼𝐴)
3230, 31nfan 1901 . . . . . . . . . 10 𝑦(𝜑𝑧 ∈ (𝐼𝐴))
33 pimincfltioc.i . . . . . . . . . . 11 (𝜑 → ∀𝑥𝐴𝑦𝐴 (𝑥𝑦 → (𝐹𝑥) ≤ (𝐹𝑦)))
3433adantr 484 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐼𝐴)) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑦 → (𝐹𝑥) ≤ (𝐹𝑦)))
35 elinel2 4104 . . . . . . . . . . 11 (𝑧 ∈ (𝐼𝐴) → 𝑧𝐴)
3635adantl 485 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐼𝐴)) → 𝑧𝐴)
3718adantr 484 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐼𝐴)) → 𝑆𝐴)
38 mnfxr 10750 . . . . . . . . . . . 12 -∞ ∈ ℝ*
3938a1i 11 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐼𝐴)) → -∞ ∈ ℝ*)
40 ressxr 10737 . . . . . . . . . . . . 13 ℝ ⊆ ℝ*
416, 8sseldd 3896 . . . . . . . . . . . . 13 (𝜑𝑆 ∈ ℝ)
4240, 41sseldi 3893 . . . . . . . . . . . 12 (𝜑𝑆 ∈ ℝ*)
4342adantr 484 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐼𝐴)) → 𝑆 ∈ ℝ*)
44 elinel1 4103 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐼𝐴) → 𝑧𝐼)
4544, 9eleqtrdi 2863 . . . . . . . . . . . 12 (𝑧 ∈ (𝐼𝐴) → 𝑧 ∈ (-∞(,]𝑆))
4645adantl 485 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝐼𝐴)) → 𝑧 ∈ (-∞(,]𝑆))
47 iocleub 42552 . . . . . . . . . . 11 ((-∞ ∈ ℝ*𝑆 ∈ ℝ*𝑧 ∈ (-∞(,]𝑆)) → 𝑧𝑆)
4839, 43, 46, 47syl3anc 1369 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐼𝐴)) → 𝑧𝑆)
4929, 32, 34, 36, 37, 48dmrelrnrel 42270 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐼𝐴)) → (𝐹𝑧) ≤ (𝐹𝑆))
5027, 49chvarvv 2006 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐼𝐴)) → (𝐹𝑥) ≤ (𝐹𝑆))
51 fveq2 6664 . . . . . . . . . . . . 13 (𝑥 = 𝑆 → (𝐹𝑥) = (𝐹𝑆))
5251breq1d 5047 . . . . . . . . . . . 12 (𝑥 = 𝑆 → ((𝐹𝑥) < 𝑅 ↔ (𝐹𝑆) < 𝑅))
5352, 1elrab2 3608 . . . . . . . . . . 11 (𝑆𝑌 ↔ (𝑆𝐴 ∧ (𝐹𝑆) < 𝑅))
548, 53sylib 221 . . . . . . . . . 10 (𝜑 → (𝑆𝐴 ∧ (𝐹𝑆) < 𝑅))
5554simprd 499 . . . . . . . . 9 (𝜑 → (𝐹𝑆) < 𝑅)
5655adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐼𝐴)) → (𝐹𝑆) < 𝑅)
5717, 20, 22, 50, 56xrlelttrd 12608 . . . . . . 7 ((𝜑𝑥 ∈ (𝐼𝐴)) → (𝐹𝑥) < 𝑅)
5814, 57jca 515 . . . . . 6 ((𝜑𝑥 ∈ (𝐼𝐴)) → (𝑥𝐴 ∧ (𝐹𝑥) < 𝑅))
591rabeq2i 3401 . . . . . 6 (𝑥𝑌 ↔ (𝑥𝐴 ∧ (𝐹𝑥) < 𝑅))
6058, 59sylibr 237 . . . . 5 ((𝜑𝑥 ∈ (𝐼𝐴)) → 𝑥𝑌)
6160ex 416 . . . 4 (𝜑 → (𝑥 ∈ (𝐼𝐴) → 𝑥𝑌))
6212, 61ralrimi 3145 . . 3 (𝜑 → ∀𝑥 ∈ (𝐼𝐴)𝑥𝑌)
6328nfci 2903 . . . 4 𝑥(𝐼𝐴)
64 nfrab1 3303 . . . . 5 𝑥{𝑥𝐴 ∣ (𝐹𝑥) < 𝑅}
651, 64nfcxfr 2918 . . . 4 𝑥𝑌
6663, 65dfss3f 3886 . . 3 ((𝐼𝐴) ⊆ 𝑌 ↔ ∀𝑥 ∈ (𝐼𝐴)𝑥𝑌)
6762, 66sylibr 237 . 2 (𝜑 → (𝐼𝐴) ⊆ 𝑌)
6811, 67eqssd 3912 1 (𝜑𝑌 = (𝐼𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1539  Ⅎwnf 1786   ∈ wcel 2112  ∀wral 3071  {crab 3075   ∩ cin 3860   ⊆ wss 3861   class class class wbr 5037  ⟶wf 6337  ‘cfv 6341  (class class class)co 7157  supcsup 8951  ℝcr 10588  -∞cmnf 10725  ℝ*cxr 10726   < clt 10727   ≤ cle 10728  (,]cioc 12794 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466  ax-cnex 10645  ax-resscn 10646  ax-1cn 10647  ax-icn 10648  ax-addcl 10649  ax-addrcl 10650  ax-mulcl 10651  ax-mulrcl 10652  ax-mulcom 10653  ax-addass 10654  ax-mulass 10655  ax-distr 10656  ax-i2m1 10657  ax-1ne0 10658  ax-1rid 10659  ax-rnegex 10660  ax-rrecex 10661  ax-cnre 10662  ax-pre-lttri 10663  ax-pre-lttrn 10664  ax-pre-ltadd 10665  ax-pre-mulgt0 10666  ax-pre-sup 10667 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4803  df-br 5038  df-opab 5100  df-mpt 5118  df-id 5435  df-po 5448  df-so 5449  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7115  df-ov 7160  df-oprab 7161  df-mpo 7162  df-er 8306  df-en 8542  df-dom 8543  df-sdom 8544  df-sup 8953  df-pnf 10729  df-mnf 10730  df-xr 10731  df-ltxr 10732  df-le 10733  df-sub 10924  df-neg 10925  df-ioc 12798 This theorem is referenced by:  incsmflem  43787
 Copyright terms: Public domain W3C validator