Theorem prcdnql 7435

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.

Step	Hyp	Ref	Expression
1		ltrelnq 7316	. . . . . 6 ⊢ <Q ⊆ (Q × Q)
2	1	brel 4661	. . . . 5 ⊢ (𝐶 <Q 𝐵 → (𝐶 ∈ Q ∧ 𝐵 ∈ Q))
3	2	simpld 111	. . . 4 ⊢ (𝐶 <Q 𝐵 → 𝐶 ∈ Q)
4	3	adantl 275	. . 3 ⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) ∧ 𝐶 <Q 𝐵) → 𝐶 ∈ Q)
5		breq1 3990	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (𝑐 <Q 𝐵 ↔ 𝐶 <Q 𝐵))
6		eleq1 2233	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (𝑐 ∈ 𝐿 ↔ 𝐶 ∈ 𝐿))
7	5, 6	imbi12d 233	. . . . . 6 ⊢ (𝑐 = 𝐶 → ((𝑐 <Q 𝐵 → 𝑐 ∈ 𝐿) ↔ (𝐶 <Q 𝐵 → 𝐶 ∈ 𝐿)))
8	7	imbi2d 229	. . . . 5 ⊢ (𝑐 = 𝐶 → (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → (𝑐 <Q 𝐵 → 𝑐 ∈ 𝐿)) ↔ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → (𝐶 <Q 𝐵 → 𝐶 ∈ 𝐿))))
9	1	brel 4661	. . . . . . . . 9 ⊢ (𝑐 <Q 𝐵 → (𝑐 ∈ Q ∧ 𝐵 ∈ Q))
10	9	ancomd 265	. . . . . . . 8 ⊢ (𝑐 <Q 𝐵 → (𝐵 ∈ Q ∧ 𝑐 ∈ Q))
11		an42 582	. . . . . . . . 9 ⊢ (((𝐵 ∈ Q ∧ 𝑐 ∈ Q) ∧ (𝐵 ∈ 𝐿 ∧ ⟨𝐿, 𝑈⟩ ∈ P)) ↔ ((𝐵 ∈ Q ∧ 𝐵 ∈ 𝐿) ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑐 ∈ Q)))
12		breq2 3991	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝐵 → (𝑐 <Q 𝑏 ↔ 𝑐 <Q 𝐵))
13		eleq1 2233	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝐵 → (𝑏 ∈ 𝐿 ↔ 𝐵 ∈ 𝐿))
14	12, 13	anbi12d 470	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝐵 → ((𝑐 <Q 𝑏 ∧ 𝑏 ∈ 𝐿) ↔ (𝑐 <Q 𝐵 ∧ 𝐵 ∈ 𝐿)))
15	14	rspcev 2834	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ Q ∧ (𝑐 <Q 𝐵 ∧ 𝐵 ∈ 𝐿)) → ∃𝑏 ∈ Q (𝑐 <Q 𝑏 ∧ 𝑏 ∈ 𝐿))
16		elinp 7425	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝐿, 𝑈⟩ ∈ P ↔ (((𝐿 ⊆ Q ∧ 𝑈 ⊆ Q) ∧ (∃𝑐 ∈ Q 𝑐 ∈ 𝐿 ∧ ∃𝑏 ∈ Q 𝑏 ∈ 𝑈)) ∧ ((∀𝑐 ∈ Q (𝑐 ∈ 𝐿 ↔ ∃𝑏 ∈ Q (𝑐 <Q 𝑏 ∧ 𝑏 ∈ 𝐿)) ∧ ∀𝑏 ∈ Q (𝑏 ∈ 𝑈 ↔ ∃𝑐 ∈ Q (𝑐 <Q 𝑏 ∧ 𝑐 ∈ 𝑈))) ∧ ∀𝑐 ∈ Q ¬ (𝑐 ∈ 𝐿 ∧ 𝑐 ∈ 𝑈) ∧ ∀𝑐 ∈ Q ∀𝑏 ∈ Q (𝑐 <Q 𝑏 → (𝑐 ∈ 𝐿 ∨ 𝑏 ∈ 𝑈)))))
17		simpr1l 1049	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐿 ⊆ Q ∧ 𝑈 ⊆ Q) ∧ (∃𝑐 ∈ Q 𝑐 ∈ 𝐿 ∧ ∃𝑏 ∈ Q 𝑏 ∈ 𝑈)) ∧ ((∀𝑐 ∈ Q (𝑐 ∈ 𝐿 ↔ ∃𝑏 ∈ Q (𝑐 <Q 𝑏 ∧ 𝑏 ∈ 𝐿)) ∧ ∀𝑏 ∈ Q (𝑏 ∈ 𝑈 ↔ ∃𝑐 ∈ Q (𝑐 <Q 𝑏 ∧ 𝑐 ∈ 𝑈))) ∧ ∀𝑐 ∈ Q ¬ (𝑐 ∈ 𝐿 ∧ 𝑐 ∈ 𝑈) ∧ ∀𝑐 ∈ Q ∀𝑏 ∈ Q (𝑐 <Q 𝑏 → (𝑐 ∈ 𝐿 ∨ 𝑏 ∈ 𝑈)))) → ∀𝑐 ∈ Q (𝑐 ∈ 𝐿 ↔ ∃𝑏 ∈ Q (𝑐 <Q 𝑏 ∧ 𝑏 ∈ 𝐿)))
18	16, 17	sylbi 120	. . . . . . . . . . . . . . 15 ⊢ (⟨𝐿, 𝑈⟩ ∈ P → ∀𝑐 ∈ Q (𝑐 ∈ 𝐿 ↔ ∃𝑏 ∈ Q (𝑐 <Q 𝑏 ∧ 𝑏 ∈ 𝐿)))
19	18	r19.21bi 2558	. . . . . . . . . . . . . 14 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑐 ∈ Q) → (𝑐 ∈ 𝐿 ↔ ∃𝑏 ∈ Q (𝑐 <Q 𝑏 ∧ 𝑏 ∈ 𝐿)))
20	15, 19	syl5ibrcom 156	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ Q ∧ (𝑐 <Q 𝐵 ∧ 𝐵 ∈ 𝐿)) → ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑐 ∈ Q) → 𝑐 ∈ 𝐿))
21	20	3impb 1194	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ Q ∧ 𝑐 <Q 𝐵 ∧ 𝐵 ∈ 𝐿) → ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑐 ∈ Q) → 𝑐 ∈ 𝐿))
22	21	3com12 1202	. . . . . . . . . . 11 ⊢ ((𝑐 <Q 𝐵 ∧ 𝐵 ∈ Q ∧ 𝐵 ∈ 𝐿) → ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑐 ∈ Q) → 𝑐 ∈ 𝐿))
23	22	3expib 1201	. . . . . . . . . 10 ⊢ (𝑐 <Q 𝐵 → ((𝐵 ∈ Q ∧ 𝐵 ∈ 𝐿) → ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑐 ∈ Q) → 𝑐 ∈ 𝐿)))
24	23	impd 252	. . . . . . . . 9 ⊢ (𝑐 <Q 𝐵 → (((𝐵 ∈ Q ∧ 𝐵 ∈ 𝐿) ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑐 ∈ Q)) → 𝑐 ∈ 𝐿))
25	11, 24	syl5bi 151	. . . . . . . 8 ⊢ (𝑐 <Q 𝐵 → (((𝐵 ∈ Q ∧ 𝑐 ∈ Q) ∧ (𝐵 ∈ 𝐿 ∧ ⟨𝐿, 𝑈⟩ ∈ P)) → 𝑐 ∈ 𝐿))
26	10, 25	mpand 427	. . . . . . 7 ⊢ (𝑐 <Q 𝐵 → ((𝐵 ∈ 𝐿 ∧ ⟨𝐿, 𝑈⟩ ∈ P) → 𝑐 ∈ 𝐿))
27	26	com12 30	. . . . . 6 ⊢ ((𝐵 ∈ 𝐿 ∧ ⟨𝐿, 𝑈⟩ ∈ P) → (𝑐 <Q 𝐵 → 𝑐 ∈ 𝐿))
28	27	ancoms 266	. . . . 5 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → (𝑐 <Q 𝐵 → 𝑐 ∈ 𝐿))
29	8, 28	vtoclg 2790	. . . 4 ⊢ (𝐶 ∈ Q → ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → (𝐶 <Q 𝐵 → 𝐶 ∈ 𝐿)))
30	29	impd 252	. . 3 ⊢ (𝐶 ∈ Q → (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) ∧ 𝐶 <Q 𝐵) → 𝐶 ∈ 𝐿))
31	4, 30	mpcom 36	. 2 ⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) ∧ 𝐶 <Q 𝐵) → 𝐶 ∈ 𝐿)
32	31	ex 114	1 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → (𝐶 <Q 𝐵 → 𝐶 ∈ 𝐿))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 703   ∧ w3a 973   = wceq 1348   ∈ wcel 2141  ∀wral 2448  ∃wrex 2449   ⊆ wss 3121  ⟨cop 3584   class class class wbr 3987  Qcnq 7231   <_Q cltq 7236  Pcnp 7242

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-coll 4102  ax-sep 4105  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-iinf 4570

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  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-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-iun 3873  df-br 3988  df-opab 4049  df-mpt 4050  df-id 4276  df-iom 4573  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-qs 6516  df-ni 7255  df-nqqs 7299  df-ltnqqs 7304  df-inp 7417

This theorem is referenced by:  prubl  7437  addnqprllem  7478  nqprl  7502  mulnqprl  7519  distrlem4prl  7535  ltprordil  7540  1idprl  7541  ltpopr  7546  ltaddpr  7548  ltexprlemlol  7553  ltexprlemfl  7560  ltexprlemrl  7561  aptiprleml  7590  aptiprlemu  7591  archrecpr  7615  caucvgprprlemml  7645  suplocexprlemrl  7668  suplocexprlemloc  7672