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

Theorem ivthinclemloc 13030
Description: Lemma for ivthinc 13032. Locatedness. (Contributed by Jim Kingdon, 18-Feb-2024.)
Hypotheses
Ref Expression
ivth.1 (𝜑𝐴 ∈ ℝ)
ivth.2 (𝜑𝐵 ∈ ℝ)
ivth.3 (𝜑𝑈 ∈ ℝ)
ivth.4 (𝜑𝐴 < 𝐵)
ivth.5 (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)
ivth.7 (𝜑𝐹 ∈ (𝐷cn→ℂ))
ivth.8 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)
ivth.9 (𝜑 → ((𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))
ivthinc.i (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹𝑥) < (𝐹𝑦))
ivthinclem.l 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹𝑤) < 𝑈}
ivthinclem.r 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹𝑤)}
Assertion
Ref Expression
ivthinclemloc (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞𝐿𝑟𝑅)))
Distinct variable groups:   𝐴,𝑟,𝑤   𝑥,𝐴,𝑦,𝑟   𝐵,𝑟,𝑤   𝑥,𝐵,𝑦   𝑤,𝐹   𝑥,𝐹,𝑦   𝑤,𝑈   𝜑,𝑞,𝑟,𝑥,𝑦   𝑤,𝑞
Allowed substitution hints:   𝜑(𝑤)   𝐴(𝑞)   𝐵(𝑞)   𝐷(𝑥,𝑦,𝑤,𝑟,𝑞)   𝑅(𝑥,𝑦,𝑤,𝑟,𝑞)   𝑈(𝑥,𝑦,𝑟,𝑞)   𝐹(𝑟,𝑞)   𝐿(𝑥,𝑦,𝑤,𝑟,𝑞)

Proof of Theorem ivthinclemloc
StepHypRef Expression
1 simpr 109 . . . . . 6 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → 𝑞 < 𝑟)
2 breq2 3969 . . . . . . . 8 (𝑦 = 𝑟 → (𝑞 < 𝑦𝑞 < 𝑟))
3 fveq2 5468 . . . . . . . . 9 (𝑦 = 𝑟 → (𝐹𝑦) = (𝐹𝑟))
43breq2d 3977 . . . . . . . 8 (𝑦 = 𝑟 → ((𝐹𝑞) < (𝐹𝑦) ↔ (𝐹𝑞) < (𝐹𝑟)))
52, 4imbi12d 233 . . . . . . 7 (𝑦 = 𝑟 → ((𝑞 < 𝑦 → (𝐹𝑞) < (𝐹𝑦)) ↔ (𝑞 < 𝑟 → (𝐹𝑞) < (𝐹𝑟))))
6 breq1 3968 . . . . . . . . . 10 (𝑥 = 𝑞 → (𝑥 < 𝑦𝑞 < 𝑦))
7 fveq2 5468 . . . . . . . . . . 11 (𝑥 = 𝑞 → (𝐹𝑥) = (𝐹𝑞))
87breq1d 3975 . . . . . . . . . 10 (𝑥 = 𝑞 → ((𝐹𝑥) < (𝐹𝑦) ↔ (𝐹𝑞) < (𝐹𝑦)))
96, 8imbi12d 233 . . . . . . . . 9 (𝑥 = 𝑞 → ((𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)) ↔ (𝑞 < 𝑦 → (𝐹𝑞) < (𝐹𝑦))))
109ralbidv 2457 . . . . . . . 8 (𝑥 = 𝑞 → (∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑞 < 𝑦 → (𝐹𝑞) < (𝐹𝑦))))
11 ivthinc.i . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹𝑥) < (𝐹𝑦))
1211expr 373 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)))
1312ralrimiva 2530 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)))
1413ralrimiva 2530 . . . . . . . . 9 (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)))
1514ad2antrr 480 . . . . . . . 8 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)))
16 simplrl 525 . . . . . . . 8 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → 𝑞 ∈ (𝐴[,]𝐵))
1710, 15, 16rspcdva 2821 . . . . . . 7 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑞 < 𝑦 → (𝐹𝑞) < (𝐹𝑦)))
18 simplrr 526 . . . . . . 7 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → 𝑟 ∈ (𝐴[,]𝐵))
195, 17, 18rspcdva 2821 . . . . . 6 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝑞 < 𝑟 → (𝐹𝑞) < (𝐹𝑟)))
201, 19mpd 13 . . . . 5 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝐹𝑞) < (𝐹𝑟))
217eleq1d 2226 . . . . . . 7 (𝑥 = 𝑞 → ((𝐹𝑥) ∈ ℝ ↔ (𝐹𝑞) ∈ ℝ))
22 ivth.8 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)
2322ralrimiva 2530 . . . . . . . 8 (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹𝑥) ∈ ℝ)
2423ad2antrr 480 . . . . . . 7 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹𝑥) ∈ ℝ)
2521, 24, 16rspcdva 2821 . . . . . 6 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝐹𝑞) ∈ ℝ)
26 fveq2 5468 . . . . . . . 8 (𝑥 = 𝑟 → (𝐹𝑥) = (𝐹𝑟))
2726eleq1d 2226 . . . . . . 7 (𝑥 = 𝑟 → ((𝐹𝑥) ∈ ℝ ↔ (𝐹𝑟) ∈ ℝ))
2827, 24, 18rspcdva 2821 . . . . . 6 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝐹𝑟) ∈ ℝ)
29 ivth.3 . . . . . . 7 (𝜑𝑈 ∈ ℝ)
3029ad2antrr 480 . . . . . 6 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → 𝑈 ∈ ℝ)
31 axltwlin 7945 . . . . . 6 (((𝐹𝑞) ∈ ℝ ∧ (𝐹𝑟) ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((𝐹𝑞) < (𝐹𝑟) → ((𝐹𝑞) < 𝑈𝑈 < (𝐹𝑟))))
3225, 28, 30, 31syl3anc 1220 . . . . 5 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ((𝐹𝑞) < (𝐹𝑟) → ((𝐹𝑞) < 𝑈𝑈 < (𝐹𝑟))))
3320, 32mpd 13 . . . 4 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ((𝐹𝑞) < 𝑈𝑈 < (𝐹𝑟)))
3416adantr 274 . . . . . . 7 ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ (𝐹𝑞) < 𝑈) → 𝑞 ∈ (𝐴[,]𝐵))
35 simpr 109 . . . . . . 7 ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ (𝐹𝑞) < 𝑈) → (𝐹𝑞) < 𝑈)
36 fveq2 5468 . . . . . . . . 9 (𝑤 = 𝑞 → (𝐹𝑤) = (𝐹𝑞))
3736breq1d 3975 . . . . . . . 8 (𝑤 = 𝑞 → ((𝐹𝑤) < 𝑈 ↔ (𝐹𝑞) < 𝑈))
38 ivthinclem.l . . . . . . . 8 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹𝑤) < 𝑈}
3937, 38elrab2 2871 . . . . . . 7 (𝑞𝐿 ↔ (𝑞 ∈ (𝐴[,]𝐵) ∧ (𝐹𝑞) < 𝑈))
4034, 35, 39sylanbrc 414 . . . . . 6 ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ (𝐹𝑞) < 𝑈) → 𝑞𝐿)
4140ex 114 . . . . 5 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ((𝐹𝑞) < 𝑈𝑞𝐿))
4218adantr 274 . . . . . . 7 ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ 𝑈 < (𝐹𝑟)) → 𝑟 ∈ (𝐴[,]𝐵))
43 simpr 109 . . . . . . 7 ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ 𝑈 < (𝐹𝑟)) → 𝑈 < (𝐹𝑟))
44 fveq2 5468 . . . . . . . . 9 (𝑤 = 𝑟 → (𝐹𝑤) = (𝐹𝑟))
4544breq2d 3977 . . . . . . . 8 (𝑤 = 𝑟 → (𝑈 < (𝐹𝑤) ↔ 𝑈 < (𝐹𝑟)))
46 ivthinclem.r . . . . . . . 8 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹𝑤)}
4745, 46elrab2 2871 . . . . . . 7 (𝑟𝑅 ↔ (𝑟 ∈ (𝐴[,]𝐵) ∧ 𝑈 < (𝐹𝑟)))
4842, 43, 47sylanbrc 414 . . . . . 6 ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ 𝑈 < (𝐹𝑟)) → 𝑟𝑅)
4948ex 114 . . . . 5 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝑈 < (𝐹𝑟) → 𝑟𝑅))
5041, 49orim12d 776 . . . 4 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (((𝐹𝑞) < 𝑈𝑈 < (𝐹𝑟)) → (𝑞𝐿𝑟𝑅)))
5133, 50mpd 13 . . 3 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝑞𝐿𝑟𝑅))
5251ex 114 . 2 ((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) → (𝑞 < 𝑟 → (𝑞𝐿𝑟𝑅)))
5352ralrimivva 2539 1 (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞𝐿𝑟𝑅)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wo 698   = wceq 1335  wcel 2128  wral 2435  {crab 2439  wss 3102   class class class wbr 3965  cfv 5170  (class class class)co 5824  cc 7730  cr 7731   < clt 7912  [,]cicc 9795  cnccncf 12968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4496  ax-cnex 7823  ax-resscn 7824  ax-pre-ltwlin 7845
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-xp 4592  df-iota 5135  df-fv 5178  df-pnf 7914  df-mnf 7915  df-ltxr 7917
This theorem is referenced by:  ivthinclemex  13031
  Copyright terms: Public domain W3C validator