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

Theorem ixxss12 12746
Description: Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro, 28-Apr-2015.)
Hypotheses
Ref Expression
ixx.1 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})
ixxss12.2 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧𝑧𝑈𝑦)})
ixxss12.3 ((𝐴 ∈ ℝ*𝐶 ∈ ℝ*𝑤 ∈ ℝ*) → ((𝐴𝑊𝐶𝐶𝑇𝑤) → 𝐴𝑅𝑤))
ixxss12.4 ((𝑤 ∈ ℝ*𝐷 ∈ ℝ*𝐵 ∈ ℝ*) → ((𝑤𝑈𝐷𝐷𝑋𝐵) → 𝑤𝑆𝐵))
Assertion
Ref Expression
ixxss12 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) → (𝐶𝑃𝐷) ⊆ (𝐴𝑂𝐵))
Distinct variable groups:   𝑥,𝑤,𝑦,𝑧,𝐴   𝑤,𝐶,𝑥,𝑦,𝑧   𝑤,𝐷,𝑥,𝑦,𝑧   𝑤,𝑂   𝑤,𝐵,𝑥,𝑦,𝑧   𝑤,𝑃   𝑥,𝑅,𝑦,𝑧   𝑥,𝑆,𝑦,𝑧   𝑥,𝑇,𝑦,𝑧   𝑥,𝑈,𝑦,𝑧   𝑤,𝑊   𝑤,𝑋
Allowed substitution hints:   𝑃(𝑥,𝑦,𝑧)   𝑅(𝑤)   𝑆(𝑤)   𝑇(𝑤)   𝑈(𝑤)   𝑂(𝑥,𝑦,𝑧)   𝑊(𝑥,𝑦,𝑧)   𝑋(𝑥,𝑦,𝑧)

Proof of Theorem ixxss12
StepHypRef Expression
1 ixxss12.2 . . . . . . . 8 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑇𝑧𝑧𝑈𝑦)})
21elixx3g 12739 . . . . . . 7 (𝑤 ∈ (𝐶𝑃𝐷) ↔ ((𝐶 ∈ ℝ*𝐷 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝐶𝑇𝑤𝑤𝑈𝐷)))
32simplbi 501 . . . . . 6 (𝑤 ∈ (𝐶𝑃𝐷) → (𝐶 ∈ ℝ*𝐷 ∈ ℝ*𝑤 ∈ ℝ*))
43adantl 485 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → (𝐶 ∈ ℝ*𝐷 ∈ ℝ*𝑤 ∈ ℝ*))
54simp3d 1141 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝑤 ∈ ℝ*)
6 simplrl 776 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝐴𝑊𝐶)
72simprbi 500 . . . . . . 7 (𝑤 ∈ (𝐶𝑃𝐷) → (𝐶𝑇𝑤𝑤𝑈𝐷))
87adantl 485 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → (𝐶𝑇𝑤𝑤𝑈𝐷))
98simpld 498 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝐶𝑇𝑤)
10 simplll 774 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝐴 ∈ ℝ*)
114simp1d 1139 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝐶 ∈ ℝ*)
12 ixxss12.3 . . . . . 6 ((𝐴 ∈ ℝ*𝐶 ∈ ℝ*𝑤 ∈ ℝ*) → ((𝐴𝑊𝐶𝐶𝑇𝑤) → 𝐴𝑅𝑤))
1310, 11, 5, 12syl3anc 1368 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → ((𝐴𝑊𝐶𝐶𝑇𝑤) → 𝐴𝑅𝑤))
146, 9, 13mp2and 698 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝐴𝑅𝑤)
158simprd 499 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝑤𝑈𝐷)
16 simplrr 777 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝐷𝑋𝐵)
174simp2d 1140 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝐷 ∈ ℝ*)
18 simpllr 775 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝐵 ∈ ℝ*)
19 ixxss12.4 . . . . . 6 ((𝑤 ∈ ℝ*𝐷 ∈ ℝ*𝐵 ∈ ℝ*) → ((𝑤𝑈𝐷𝐷𝑋𝐵) → 𝑤𝑆𝐵))
205, 17, 18, 19syl3anc 1368 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → ((𝑤𝑈𝐷𝐷𝑋𝐵) → 𝑤𝑆𝐵))
2115, 16, 20mp2and 698 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝑤𝑆𝐵)
22 ixx.1 . . . . . 6 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})
2322elixx1 12735 . . . . 5 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ*𝐴𝑅𝑤𝑤𝑆𝐵)))
2423ad2antrr 725 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → (𝑤 ∈ (𝐴𝑂𝐵) ↔ (𝑤 ∈ ℝ*𝐴𝑅𝑤𝑤𝑆𝐵)))
255, 14, 21, 24mpbir3and 1339 . . 3 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) ∧ 𝑤 ∈ (𝐶𝑃𝐷)) → 𝑤 ∈ (𝐴𝑂𝐵))
2625ex 416 . 2 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) → (𝑤 ∈ (𝐶𝑃𝐷) → 𝑤 ∈ (𝐴𝑂𝐵)))
2726ssrdv 3948 1 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑊𝐶𝐷𝑋𝐵)) → (𝐶𝑃𝐷) ⊆ (𝐴𝑂𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2114  {crab 3134  wss 3908   class class class wbr 5042  (class class class)co 7140  cmpo 7142  *cxr 10663
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-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-cnex 10582  ax-resscn 10583
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  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-ral 3135  df-rex 3136  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-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  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-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-fv 6342  df-ov 7143  df-oprab 7144  df-mpo 7145  df-1st 7675  df-2nd 7676  df-xr 10668
This theorem is referenced by:  iccss  12793  iccssioo  12794  icossico  12795  iccss2  12796  iccssico  12797  iocssioo  12817  icossioo  12818  ioossioo  12819
  Copyright terms: Public domain W3C validator