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

Theorem ivthinclemloc 13413
Description: Lemma for ivthinc 13415. 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 3993 . . . . . . . 8 (𝑦 = 𝑟 → (𝑞 < 𝑦𝑞 < 𝑟))
3 fveq2 5496 . . . . . . . . 9 (𝑦 = 𝑟 → (𝐹𝑦) = (𝐹𝑟))
43breq2d 4001 . . . . . . . 8 (𝑦 = 𝑟 → ((𝐹𝑞) < (𝐹𝑦) ↔ (𝐹𝑞) < (𝐹𝑟)))
52, 4imbi12d 233 . . . . . . 7 (𝑦 = 𝑟 → ((𝑞 < 𝑦 → (𝐹𝑞) < (𝐹𝑦)) ↔ (𝑞 < 𝑟 → (𝐹𝑞) < (𝐹𝑟))))
6 breq1 3992 . . . . . . . . . 10 (𝑥 = 𝑞 → (𝑥 < 𝑦𝑞 < 𝑦))
7 fveq2 5496 . . . . . . . . . . 11 (𝑥 = 𝑞 → (𝐹𝑥) = (𝐹𝑞))
87breq1d 3999 . . . . . . . . . 10 (𝑥 = 𝑞 → ((𝐹𝑥) < (𝐹𝑦) ↔ (𝐹𝑞) < (𝐹𝑦)))
96, 8imbi12d 233 . . . . . . . . 9 (𝑥 = 𝑞 → ((𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)) ↔ (𝑞 < 𝑦 → (𝐹𝑞) < (𝐹𝑦))))
109ralbidv 2470 . . . . . . . 8 (𝑥 = 𝑞 → (∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑞 < 𝑦 → (𝐹𝑞) < (𝐹𝑦))))
11 ivthinc.i . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹𝑥) < (𝐹𝑦))
1211expr 373 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)))
1312ralrimiva 2543 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)))
1413ralrimiva 2543 . . . . . . . . 9 (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)))
1514ad2antrr 485 . . . . . . . 8 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹𝑥) < (𝐹𝑦)))
16 simplrl 530 . . . . . . . 8 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → 𝑞 ∈ (𝐴[,]𝐵))
1710, 15, 16rspcdva 2839 . . . . . . 7 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑞 < 𝑦 → (𝐹𝑞) < (𝐹𝑦)))
18 simplrr 531 . . . . . . 7 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → 𝑟 ∈ (𝐴[,]𝐵))
195, 17, 18rspcdva 2839 . . . . . 6 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝑞 < 𝑟 → (𝐹𝑞) < (𝐹𝑟)))
201, 19mpd 13 . . . . 5 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝐹𝑞) < (𝐹𝑟))
217eleq1d 2239 . . . . . . 7 (𝑥 = 𝑞 → ((𝐹𝑥) ∈ ℝ ↔ (𝐹𝑞) ∈ ℝ))
22 ivth.8 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℝ)
2322ralrimiva 2543 . . . . . . . 8 (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹𝑥) ∈ ℝ)
2423ad2antrr 485 . . . . . . 7 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹𝑥) ∈ ℝ)
2521, 24, 16rspcdva 2839 . . . . . 6 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝐹𝑞) ∈ ℝ)
26 fveq2 5496 . . . . . . . 8 (𝑥 = 𝑟 → (𝐹𝑥) = (𝐹𝑟))
2726eleq1d 2239 . . . . . . 7 (𝑥 = 𝑟 → ((𝐹𝑥) ∈ ℝ ↔ (𝐹𝑟) ∈ ℝ))
2827, 24, 18rspcdva 2839 . . . . . 6 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝐹𝑟) ∈ ℝ)
29 ivth.3 . . . . . . 7 (𝜑𝑈 ∈ ℝ)
3029ad2antrr 485 . . . . . 6 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → 𝑈 ∈ ℝ)
31 axltwlin 7987 . . . . . 6 (((𝐹𝑞) ∈ ℝ ∧ (𝐹𝑟) ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((𝐹𝑞) < (𝐹𝑟) → ((𝐹𝑞) < 𝑈𝑈 < (𝐹𝑟))))
3225, 28, 30, 31syl3anc 1233 . . . . 5 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ((𝐹𝑞) < (𝐹𝑟) → ((𝐹𝑞) < 𝑈𝑈 < (𝐹𝑟))))
3320, 32mpd 13 . . . 4 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ((𝐹𝑞) < 𝑈𝑈 < (𝐹𝑟)))
3416adantr 274 . . . . . . 7 ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ (𝐹𝑞) < 𝑈) → 𝑞 ∈ (𝐴[,]𝐵))
35 simpr 109 . . . . . . 7 ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ (𝐹𝑞) < 𝑈) → (𝐹𝑞) < 𝑈)
36 fveq2 5496 . . . . . . . . 9 (𝑤 = 𝑞 → (𝐹𝑤) = (𝐹𝑞))
3736breq1d 3999 . . . . . . . 8 (𝑤 = 𝑞 → ((𝐹𝑤) < 𝑈 ↔ (𝐹𝑞) < 𝑈))
38 ivthinclem.l . . . . . . . 8 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹𝑤) < 𝑈}
3937, 38elrab2 2889 . . . . . . 7 (𝑞𝐿 ↔ (𝑞 ∈ (𝐴[,]𝐵) ∧ (𝐹𝑞) < 𝑈))
4034, 35, 39sylanbrc 415 . . . . . 6 ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ (𝐹𝑞) < 𝑈) → 𝑞𝐿)
4140ex 114 . . . . 5 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → ((𝐹𝑞) < 𝑈𝑞𝐿))
4218adantr 274 . . . . . . 7 ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ 𝑈 < (𝐹𝑟)) → 𝑟 ∈ (𝐴[,]𝐵))
43 simpr 109 . . . . . . 7 ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ 𝑈 < (𝐹𝑟)) → 𝑈 < (𝐹𝑟))
44 fveq2 5496 . . . . . . . . 9 (𝑤 = 𝑟 → (𝐹𝑤) = (𝐹𝑟))
4544breq2d 4001 . . . . . . . 8 (𝑤 = 𝑟 → (𝑈 < (𝐹𝑤) ↔ 𝑈 < (𝐹𝑟)))
46 ivthinclem.r . . . . . . . 8 𝑅 = {𝑤 ∈ (𝐴[,]𝐵) ∣ 𝑈 < (𝐹𝑤)}
4745, 46elrab2 2889 . . . . . . 7 (𝑟𝑅 ↔ (𝑟 ∈ (𝐴[,]𝐵) ∧ 𝑈 < (𝐹𝑟)))
4842, 43, 47sylanbrc 415 . . . . . 6 ((((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) ∧ 𝑈 < (𝐹𝑟)) → 𝑟𝑅)
4948ex 114 . . . . 5 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝑈 < (𝐹𝑟) → 𝑟𝑅))
5041, 49orim12d 781 . . . 4 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (((𝐹𝑞) < 𝑈𝑈 < (𝐹𝑟)) → (𝑞𝐿𝑟𝑅)))
5133, 50mpd 13 . . 3 (((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) ∧ 𝑞 < 𝑟) → (𝑞𝐿𝑟𝑅))
5251ex 114 . 2 ((𝜑 ∧ (𝑞 ∈ (𝐴[,]𝐵) ∧ 𝑟 ∈ (𝐴[,]𝐵))) → (𝑞 < 𝑟 → (𝑞𝐿𝑟𝑅)))
5352ralrimivva 2552 1 (𝜑 → ∀𝑞 ∈ (𝐴[,]𝐵)∀𝑟 ∈ (𝐴[,]𝐵)(𝑞 < 𝑟 → (𝑞𝐿𝑟𝑅)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wo 703   = wceq 1348  wcel 2141  wral 2448  {crab 2452  wss 3121   class class class wbr 3989  cfv 5198  (class class class)co 5853  cc 7772  cr 7773   < clt 7954  [,]cicc 9848  cnccncf 13351
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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-cnex 7865  ax-resscn 7866  ax-pre-ltwlin 7887
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-rab 2457  df-v 2732  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-opab 4051  df-xp 4617  df-iota 5160  df-fv 5206  df-pnf 7956  df-mnf 7957  df-ltxr 7959
This theorem is referenced by:  ivthinclemex  13414
  Copyright terms: Public domain W3C validator