ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ixxss2 GIF version

Theorem ixxss2 9386
Description: Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
Hypotheses
Ref Expression
ixxssixx.1 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})
ixxss2.2 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑇𝑦)})
ixxss2.3 ((𝑤 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝑤𝑇𝐵𝐵𝑊𝐶) → 𝑤𝑆𝐶))
Assertion
Ref Expression
ixxss2 ((𝐶 ∈ ℝ*𝐵𝑊𝐶) → (𝐴𝑃𝐵) ⊆ (𝐴𝑂𝐶))
Distinct variable groups:   𝑥,𝑤,𝑦,𝑧,𝐴   𝑤,𝐶,𝑥,𝑦,𝑧   𝑤,𝑂,𝑥   𝑤,𝐵,𝑥,𝑦,𝑧   𝑤,𝑃   𝑥,𝑅,𝑦,𝑧   𝑥,𝑆,𝑦,𝑧   𝑥,𝑇,𝑦,𝑧   𝑤,𝑊
Allowed substitution hints:   𝑃(𝑥,𝑦,𝑧)   𝑅(𝑤)   𝑆(𝑤)   𝑇(𝑤)   𝑂(𝑦,𝑧)   𝑊(𝑥,𝑦,𝑧)

Proof of Theorem ixxss2
StepHypRef Expression
1 ixxss2.2 . . . . . . . 8 𝑃 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑇𝑦)})
21elixx3g 9382 . . . . . . 7 (𝑤 ∈ (𝐴𝑃𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝐴𝑅𝑤𝑤𝑇𝐵)))
32simplbi 269 . . . . . 6 (𝑤 ∈ (𝐴𝑃𝐵) → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑤 ∈ ℝ*))
43adantl 272 . . . . 5 (((𝐶 ∈ ℝ*𝐵𝑊𝐶) ∧ 𝑤 ∈ (𝐴𝑃𝐵)) → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑤 ∈ ℝ*))
54simp3d 958 . . . 4 (((𝐶 ∈ ℝ*𝐵𝑊𝐶) ∧ 𝑤 ∈ (𝐴𝑃𝐵)) → 𝑤 ∈ ℝ*)
62simprbi 270 . . . . . 6 (𝑤 ∈ (𝐴𝑃𝐵) → (𝐴𝑅𝑤𝑤𝑇𝐵))
76adantl 272 . . . . 5 (((𝐶 ∈ ℝ*𝐵𝑊𝐶) ∧ 𝑤 ∈ (𝐴𝑃𝐵)) → (𝐴𝑅𝑤𝑤𝑇𝐵))
87simpld 111 . . . 4 (((𝐶 ∈ ℝ*𝐵𝑊𝐶) ∧ 𝑤 ∈ (𝐴𝑃𝐵)) → 𝐴𝑅𝑤)
97simprd 113 . . . . 5 (((𝐶 ∈ ℝ*𝐵𝑊𝐶) ∧ 𝑤 ∈ (𝐴𝑃𝐵)) → 𝑤𝑇𝐵)
10 simplr 498 . . . . 5 (((𝐶 ∈ ℝ*𝐵𝑊𝐶) ∧ 𝑤 ∈ (𝐴𝑃𝐵)) → 𝐵𝑊𝐶)
114simp2d 957 . . . . . 6 (((𝐶 ∈ ℝ*𝐵𝑊𝐶) ∧ 𝑤 ∈ (𝐴𝑃𝐵)) → 𝐵 ∈ ℝ*)
12 simpll 497 . . . . . 6 (((𝐶 ∈ ℝ*𝐵𝑊𝐶) ∧ 𝑤 ∈ (𝐴𝑃𝐵)) → 𝐶 ∈ ℝ*)
13 ixxss2.3 . . . . . 6 ((𝑤 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝑤𝑇𝐵𝐵𝑊𝐶) → 𝑤𝑆𝐶))
145, 11, 12, 13syl3anc 1175 . . . . 5 (((𝐶 ∈ ℝ*𝐵𝑊𝐶) ∧ 𝑤 ∈ (𝐴𝑃𝐵)) → ((𝑤𝑇𝐵𝐵𝑊𝐶) → 𝑤𝑆𝐶))
159, 10, 14mp2and 425 . . . 4 (((𝐶 ∈ ℝ*𝐵𝑊𝐶) ∧ 𝑤 ∈ (𝐴𝑃𝐵)) → 𝑤𝑆𝐶)
164simp1d 956 . . . . 5 (((𝐶 ∈ ℝ*𝐵𝑊𝐶) ∧ 𝑤 ∈ (𝐴𝑃𝐵)) → 𝐴 ∈ ℝ*)
17 ixxssixx.1 . . . . . 6 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧𝑧𝑆𝑦)})
1817elixx1 9378 . . . . 5 ((𝐴 ∈ ℝ*𝐶 ∈ ℝ*) → (𝑤 ∈ (𝐴𝑂𝐶) ↔ (𝑤 ∈ ℝ*𝐴𝑅𝑤𝑤𝑆𝐶)))
1916, 12, 18syl2anc 404 . . . 4 (((𝐶 ∈ ℝ*𝐵𝑊𝐶) ∧ 𝑤 ∈ (𝐴𝑃𝐵)) → (𝑤 ∈ (𝐴𝑂𝐶) ↔ (𝑤 ∈ ℝ*𝐴𝑅𝑤𝑤𝑆𝐶)))
205, 8, 15, 19mpbir3and 1127 . . 3 (((𝐶 ∈ ℝ*𝐵𝑊𝐶) ∧ 𝑤 ∈ (𝐴𝑃𝐵)) → 𝑤 ∈ (𝐴𝑂𝐶))
2120ex 114 . 2 ((𝐶 ∈ ℝ*𝐵𝑊𝐶) → (𝑤 ∈ (𝐴𝑃𝐵) → 𝑤 ∈ (𝐴𝑂𝐶)))
2221ssrdv 3034 1 ((𝐶 ∈ ℝ*𝐵𝑊𝐶) → (𝐴𝑃𝐵) ⊆ (𝐴𝑂𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 925   = wceq 1290  wcel 1439  {crab 2364  wss 3002   class class class wbr 3853  (class class class)co 5668  cmpt2 5670  *cxr 7584
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-13 1450  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3965  ax-pow 4017  ax-pr 4047  ax-un 4271  ax-setind 4368  ax-cnex 7499  ax-resscn 7500
This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-ral 2365  df-rex 2366  df-rab 2369  df-v 2624  df-sbc 2844  df-dif 3004  df-un 3006  df-in 3008  df-ss 3015  df-pw 3437  df-sn 3458  df-pr 3459  df-op 3461  df-uni 3662  df-br 3854  df-opab 3908  df-id 4131  df-xp 4460  df-rel 4461  df-cnv 4462  df-co 4463  df-dm 4464  df-iota 4995  df-fun 5032  df-fv 5038  df-ov 5671  df-oprab 5672  df-mpt2 5673  df-pnf 7587  df-mnf 7588  df-xr 7589
This theorem is referenced by:  iooss2  9398
  Copyright terms: Public domain W3C validator