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

Theorem prarloclemup 7491
Description: Contracting the upper side of an interval which straddles a Dedekind cut. Lemma for prarloc 7499. (Contributed by Jim Kingdon, 10-Nov-2019.)
Assertion
Ref Expression
prarloclemup (((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P𝐴𝐿𝑃Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈 → (((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o suc 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈))))

Proof of Theorem prarloclemup
StepHypRef Expression
1 simpllr 534 . . 3 (((((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P𝐴𝐿𝑃Q)) ∧ 𝑦 ∈ ω) ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) ∧ ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o suc 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈)) → 𝑦 ∈ ω)
2 simprl 529 . . 3 (((((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P𝐴𝐿𝑃Q)) ∧ 𝑦 ∈ ω) ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) ∧ ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o suc 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈)) → (𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿)
3 simplr 528 . . 3 (((((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P𝐴𝐿𝑃Q)) ∧ 𝑦 ∈ ω) ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) ∧ ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o suc 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈)) → (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈)
4 rspe 2526 . . 3 ((𝑦 ∈ ω ∧ ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈)) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈))
51, 2, 3, 4syl12anc 1236 . 2 (((((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P𝐴𝐿𝑃Q)) ∧ 𝑦 ∈ ω) ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) ∧ ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o suc 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈)) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈))
65exp31 364 1 (((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P𝐴𝐿𝑃Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈 → (((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o suc 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 978  wcel 2148  wrex 2456  cop 3595  suc csuc 4364  ωcom 4588  (class class class)co 5872  1oc1o 6407  2oc2o 6408   +o coa 6411  [cec 6530   ~Q ceq 7275  Qcnq 7276   +Q cplq 7278   ·Q cmq 7279   ~Q0 ceq0 7282   +Q0 cplq0 7285   ·Q0 cmq0 7286  Pcnp 7287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510
This theorem depends on definitions:  df-bi 117  df-rex 2461
This theorem is referenced by:  prarloclem3step  7492
  Copyright terms: Public domain W3C validator