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

Theorem prcdnql 6582
 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 6463 . . . . . 6 <Q ⊆ (Q × Q)
21brel 4392 . . . . 5 (𝐶 <Q 𝐵 → (𝐶Q𝐵Q))
32simpld 105 . . . 4 (𝐶 <Q 𝐵𝐶Q)
43adantl 262 . . 3 (((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) ∧ 𝐶 <Q 𝐵) → 𝐶Q)
5 breq1 3767 . . . . . . 7 (𝑐 = 𝐶 → (𝑐 <Q 𝐵𝐶 <Q 𝐵))
6 eleq1 2100 . . . . . . 7 (𝑐 = 𝐶 → (𝑐𝐿𝐶𝐿))
75, 6imbi12d 223 . . . . . 6 (𝑐 = 𝐶 → ((𝑐 <Q 𝐵𝑐𝐿) ↔ (𝐶 <Q 𝐵𝐶𝐿)))
87imbi2d 219 . . . . 5 (𝑐 = 𝐶 → (((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) → (𝑐 <Q 𝐵𝑐𝐿)) ↔ ((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) → (𝐶 <Q 𝐵𝐶𝐿))))
91brel 4392 . . . . . . . . 9 (𝑐 <Q 𝐵 → (𝑐Q𝐵Q))
109ancomd 254 . . . . . . . 8 (𝑐 <Q 𝐵 → (𝐵Q𝑐Q))
11 an42 521 . . . . . . . . 9 (((𝐵Q𝑐Q) ∧ (𝐵𝐿 ∧ ⟨𝐿, 𝑈⟩ ∈ P)) ↔ ((𝐵Q𝐵𝐿) ∧ (⟨𝐿, 𝑈⟩ ∈ P𝑐Q)))
12 breq2 3768 . . . . . . . . . . . . . . . 16 (𝑏 = 𝐵 → (𝑐 <Q 𝑏𝑐 <Q 𝐵))
13 eleq1 2100 . . . . . . . . . . . . . . . 16 (𝑏 = 𝐵 → (𝑏𝐿𝐵𝐿))
1412, 13anbi12d 442 . . . . . . . . . . . . . . 15 (𝑏 = 𝐵 → ((𝑐 <Q 𝑏𝑏𝐿) ↔ (𝑐 <Q 𝐵𝐵𝐿)))
1514rspcev 2656 . . . . . . . . . . . . . 14 ((𝐵Q ∧ (𝑐 <Q 𝐵𝐵𝐿)) → ∃𝑏Q (𝑐 <Q 𝑏𝑏𝐿))
16 elinp 6572 . . . . . . . . . . . . . . . 16 (⟨𝐿, 𝑈⟩ ∈ P ↔ (((𝐿Q𝑈Q) ∧ (∃𝑐Q 𝑐𝐿 ∧ ∃𝑏Q 𝑏𝑈)) ∧ ((∀𝑐Q (𝑐𝐿 ↔ ∃𝑏Q (𝑐 <Q 𝑏𝑏𝐿)) ∧ ∀𝑏Q (𝑏𝑈 ↔ ∃𝑐Q (𝑐 <Q 𝑏𝑐𝑈))) ∧ ∀𝑐Q ¬ (𝑐𝐿𝑐𝑈) ∧ ∀𝑐Q𝑏Q (𝑐 <Q 𝑏 → (𝑐𝐿𝑏𝑈)))))
17 simpr1l 961 . . . . . . . . . . . . . . . 16 ((((𝐿Q𝑈Q) ∧ (∃𝑐Q 𝑐𝐿 ∧ ∃𝑏Q 𝑏𝑈)) ∧ ((∀𝑐Q (𝑐𝐿 ↔ ∃𝑏Q (𝑐 <Q 𝑏𝑏𝐿)) ∧ ∀𝑏Q (𝑏𝑈 ↔ ∃𝑐Q (𝑐 <Q 𝑏𝑐𝑈))) ∧ ∀𝑐Q ¬ (𝑐𝐿𝑐𝑈) ∧ ∀𝑐Q𝑏Q (𝑐 <Q 𝑏 → (𝑐𝐿𝑏𝑈)))) → ∀𝑐Q (𝑐𝐿 ↔ ∃𝑏Q (𝑐 <Q 𝑏𝑏𝐿)))
1816, 17sylbi 114 . . . . . . . . . . . . . . 15 (⟨𝐿, 𝑈⟩ ∈ P → ∀𝑐Q (𝑐𝐿 ↔ ∃𝑏Q (𝑐 <Q 𝑏𝑏𝐿)))
1918r19.21bi 2407 . . . . . . . . . . . . . 14 ((⟨𝐿, 𝑈⟩ ∈ P𝑐Q) → (𝑐𝐿 ↔ ∃𝑏Q (𝑐 <Q 𝑏𝑏𝐿)))
2015, 19syl5ibrcom 146 . . . . . . . . . . . . 13 ((𝐵Q ∧ (𝑐 <Q 𝐵𝐵𝐿)) → ((⟨𝐿, 𝑈⟩ ∈ P𝑐Q) → 𝑐𝐿))
21203impb 1100 . . . . . . . . . . . 12 ((𝐵Q𝑐 <Q 𝐵𝐵𝐿) → ((⟨𝐿, 𝑈⟩ ∈ P𝑐Q) → 𝑐𝐿))
22213com12 1108 . . . . . . . . . . 11 ((𝑐 <Q 𝐵𝐵Q𝐵𝐿) → ((⟨𝐿, 𝑈⟩ ∈ P𝑐Q) → 𝑐𝐿))
23223expib 1107 . . . . . . . . . 10 (𝑐 <Q 𝐵 → ((𝐵Q𝐵𝐿) → ((⟨𝐿, 𝑈⟩ ∈ P𝑐Q) → 𝑐𝐿)))
2423impd 242 . . . . . . . . 9 (𝑐 <Q 𝐵 → (((𝐵Q𝐵𝐿) ∧ (⟨𝐿, 𝑈⟩ ∈ P𝑐Q)) → 𝑐𝐿))
2511, 24syl5bi 141 . . . . . . . 8 (𝑐 <Q 𝐵 → (((𝐵Q𝑐Q) ∧ (𝐵𝐿 ∧ ⟨𝐿, 𝑈⟩ ∈ P)) → 𝑐𝐿))
2610, 25mpand 405 . . . . . . 7 (𝑐 <Q 𝐵 → ((𝐵𝐿 ∧ ⟨𝐿, 𝑈⟩ ∈ P) → 𝑐𝐿))
2726com12 27 . . . . . 6 ((𝐵𝐿 ∧ ⟨𝐿, 𝑈⟩ ∈ P) → (𝑐 <Q 𝐵𝑐𝐿))
2827ancoms 255 . . . . 5 ((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) → (𝑐 <Q 𝐵𝑐𝐿))
298, 28vtoclg 2613 . . . 4 (𝐶Q → ((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) → (𝐶 <Q 𝐵𝐶𝐿)))
3029impd 242 . . 3 (𝐶Q → (((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) ∧ 𝐶 <Q 𝐵) → 𝐶𝐿))
314, 30mpcom 32 . 2 (((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) ∧ 𝐶 <Q 𝐵) → 𝐶𝐿)
3231ex 108 1 ((⟨𝐿, 𝑈⟩ ∈ P𝐵𝐿) → (𝐶 <Q 𝐵𝐶𝐿))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 629   ∧ w3a 885   = wceq 1243   ∈ wcel 1393  ∀wral 2306  ∃wrex 2307   ⊆ wss 2917  ⟨cop 3378   class class class wbr 3764  Qcnq 6378
 Copyright terms: Public domain W3C validator