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

Theorem prcdnql 7304
Description: A lower cut is closed downwards under the positive fractions. (Contributed by Jim Kingdon, 28-Sep-2019.)
Assertion
Ref Expression
prcdnql ((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) → (𝐶 <Q 𝐵𝐶𝐿))

Proof of Theorem prcdnql
Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrelnq 7185 . . . . . 6 <Q ⊆ (Q × Q)
21brel 4591 . . . . 5 (𝐶 <Q 𝐵 → (𝐶Q𝐵Q))
32simpld 111 . . . 4 (𝐶 <Q 𝐵𝐶Q)
43adantl 275 . . 3 (((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) ∧ 𝐶 <Q 𝐵) → 𝐶Q)
5 breq1 3932 . . . . . . 7 (𝑐 = 𝐶 → (𝑐 <Q 𝐵𝐶 <Q 𝐵))
6 eleq1 2202 . . . . . . 7 (𝑐 = 𝐶 → (𝑐𝐿𝐶𝐿))
75, 6imbi12d 233 . . . . . 6 (𝑐 = 𝐶 → ((𝑐 <Q 𝐵𝑐𝐿) ↔ (𝐶 <Q 𝐵𝐶𝐿)))
87imbi2d 229 . . . . 5 (𝑐 = 𝐶 → (((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) → (𝑐 <Q 𝐵𝑐𝐿)) ↔ ((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) → (𝐶 <Q 𝐵𝐶𝐿))))
91brel 4591 . . . . . . . . 9 (𝑐 <Q 𝐵 → (𝑐Q𝐵Q))
109ancomd 265 . . . . . . . 8 (𝑐 <Q 𝐵 → (𝐵Q𝑐Q))
11 an42 576 . . . . . . . . 9 (((𝐵Q𝑐Q) ∧ (𝐵𝐿 ∧ ⟨𝐿, 𝑈⟩ ∈ P)) ↔ ((𝐵Q𝐵𝐿) ∧ (⟨𝐿, 𝑈⟩ ∈ P𝑐Q)))
12 breq2 3933 . . . . . . . . . . . . . . . 16 (𝑏 = 𝐵 → (𝑐 <Q 𝑏𝑐 <Q 𝐵))
13 eleq1 2202 . . . . . . . . . . . . . . . 16 (𝑏 = 𝐵 → (𝑏𝐿𝐵𝐿))
1412, 13anbi12d 464 . . . . . . . . . . . . . . 15 (𝑏 = 𝐵 → ((𝑐 <Q 𝑏𝑏𝐿) ↔ (𝑐 <Q 𝐵𝐵𝐿)))
1514rspcev 2789 . . . . . . . . . . . . . 14 ((𝐵Q ∧ (𝑐 <Q 𝐵𝐵𝐿)) → ∃𝑏Q (𝑐 <Q 𝑏𝑏𝐿))
16 elinp 7294 . . . . . . . . . . . . . . . 16 (⟨𝐿, 𝑈⟩ ∈ P ↔ (((𝐿Q𝑈Q) ∧ (∃𝑐Q 𝑐𝐿 ∧ ∃𝑏Q 𝑏𝑈)) ∧ ((∀𝑐Q (𝑐𝐿 ↔ ∃𝑏Q (𝑐 <Q 𝑏𝑏𝐿)) ∧ ∀𝑏Q (𝑏𝑈 ↔ ∃𝑐Q (𝑐 <Q 𝑏𝑐𝑈))) ∧ ∀𝑐Q ¬ (𝑐𝐿𝑐𝑈) ∧ ∀𝑐Q𝑏Q (𝑐 <Q 𝑏 → (𝑐𝐿𝑏𝑈)))))
17 simpr1l 1038 . . . . . . . . . . . . . . . 16 ((((𝐿Q𝑈Q) ∧ (∃𝑐Q 𝑐𝐿 ∧ ∃𝑏Q 𝑏𝑈)) ∧ ((∀𝑐Q (𝑐𝐿 ↔ ∃𝑏Q (𝑐 <Q 𝑏𝑏𝐿)) ∧ ∀𝑏Q (𝑏𝑈 ↔ ∃𝑐Q (𝑐 <Q 𝑏𝑐𝑈))) ∧ ∀𝑐Q ¬ (𝑐𝐿𝑐𝑈) ∧ ∀𝑐Q𝑏Q (𝑐 <Q 𝑏 → (𝑐𝐿𝑏𝑈)))) → ∀𝑐Q (𝑐𝐿 ↔ ∃𝑏Q (𝑐 <Q 𝑏𝑏𝐿)))
1816, 17sylbi 120 . . . . . . . . . . . . . . 15 (⟨𝐿, 𝑈⟩ ∈ P → ∀𝑐Q (𝑐𝐿 ↔ ∃𝑏Q (𝑐 <Q 𝑏𝑏𝐿)))
1918r19.21bi 2520 . . . . . . . . . . . . . 14 ((⟨𝐿, 𝑈⟩ ∈ P𝑐Q) → (𝑐𝐿 ↔ ∃𝑏Q (𝑐 <Q 𝑏𝑏𝐿)))
2015, 19syl5ibrcom 156 . . . . . . . . . . . . 13 ((𝐵Q ∧ (𝑐 <Q 𝐵𝐵𝐿)) → ((⟨𝐿, 𝑈⟩ ∈ P𝑐Q) → 𝑐𝐿))
21203impb 1177 . . . . . . . . . . . 12 ((𝐵Q𝑐 <Q 𝐵𝐵𝐿) → ((⟨𝐿, 𝑈⟩ ∈ P𝑐Q) → 𝑐𝐿))
22213com12 1185 . . . . . . . . . . 11 ((𝑐 <Q 𝐵𝐵Q𝐵𝐿) → ((⟨𝐿, 𝑈⟩ ∈ P𝑐Q) → 𝑐𝐿))
23223expib 1184 . . . . . . . . . 10 (𝑐 <Q 𝐵 → ((𝐵Q𝐵𝐿) → ((⟨𝐿, 𝑈⟩ ∈ P𝑐Q) → 𝑐𝐿)))
2423impd 252 . . . . . . . . 9 (𝑐 <Q 𝐵 → (((𝐵Q𝐵𝐿) ∧ (⟨𝐿, 𝑈⟩ ∈ P𝑐Q)) → 𝑐𝐿))
2511, 24syl5bi 151 . . . . . . . 8 (𝑐 <Q 𝐵 → (((𝐵Q𝑐Q) ∧ (𝐵𝐿 ∧ ⟨𝐿, 𝑈⟩ ∈ P)) → 𝑐𝐿))
2610, 25mpand 425 . . . . . . 7 (𝑐 <Q 𝐵 → ((𝐵𝐿 ∧ ⟨𝐿, 𝑈⟩ ∈ P) → 𝑐𝐿))
2726com12 30 . . . . . 6 ((𝐵𝐿 ∧ ⟨𝐿, 𝑈⟩ ∈ P) → (𝑐 <Q 𝐵𝑐𝐿))
2827ancoms 266 . . . . 5 ((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) → (𝑐 <Q 𝐵𝑐𝐿))
298, 28vtoclg 2746 . . . 4 (𝐶Q → ((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) → (𝐶 <Q 𝐵𝐶𝐿)))
3029impd 252 . . 3 (𝐶Q → (((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) ∧ 𝐶 <Q 𝐵) → 𝐶𝐿))
314, 30mpcom 36 . 2 (((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) ∧ 𝐶 <Q 𝐵) → 𝐶𝐿)
3231ex 114 1 ((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) → (𝐶 <Q 𝐵𝐶𝐿))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 697  w3a 962   = wceq 1331  wcel 1480  wral 2416  wrex 2417  wss 3071  cop 3530   class class class wbr 3929  Qcnq 7100   <Q cltq 7105  Pcnp 7111
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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-iinf 4502
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-id 4215  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-qs 6435  df-ni 7124  df-nqqs 7168  df-ltnqqs 7173  df-inp 7286
This theorem is referenced by:  prubl  7306  addnqprllem  7347  nqprl  7371  mulnqprl  7388  distrlem4prl  7404  ltprordil  7409  1idprl  7410  ltpopr  7415  ltaddpr  7417  ltexprlemlol  7422  ltexprlemfl  7429  ltexprlemrl  7430  aptiprleml  7459  aptiprlemu  7460  archrecpr  7484  caucvgprprlemml  7514  suplocexprlemrl  7537  suplocexprlemloc  7541
  Copyright terms: Public domain W3C validator