Theorem elprnql 6961

Description: An element of a positive real's lower cut is a positive fraction. (Contributed by Jim Kingdon, 28-Sep-2019.)

Assertion

Ref	Expression
elprnql	⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → 𝐵 ∈ Q)

Proof of Theorem elprnql

Step	Hyp	Ref	Expression
1		prssnql 6959	. 2 ⊢ (⟨𝐿, 𝑈⟩ ∈ P → 𝐿 ⊆ Q)
2	1	sselda 3012	1 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → 𝐵 ∈ Q)

Syntax hints:   → wi 4   ∧ wa 102   ∈ wcel 1436  ⟨cop 3428  Qcnq 6760  Pcnp 6771

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3922  ax-sep 3925  ax-pow 3977  ax-pr 4003  ax-un 4227  ax-iinf 4369

This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2616  df-sbc 2829  df-csb 2922  df-dif 2988  df-un 2990  df-in 2992  df-ss 2999  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-int 3666  df-iun 3709  df-br 3815  df-opab 3869  df-mpt 3870  df-id 4087  df-iom 4372  df-xp 4410  df-rel 4411  df-cnv 4412  df-co 4413  df-dm 4414  df-rn 4415  df-res 4416  df-ima 4417  df-iota 4937  df-fun 4974  df-fn 4975  df-f 4976  df-f1 4977  df-fo 4978  df-f1o 4979  df-fv 4980  df-qs 6231  df-ni 6784  df-nqqs 6828  df-inp 6946

This theorem is referenced by:  prubl  6966  prnmaxl  6968  prarloclemlt  6973  prarloclemlo  6974  prarloclem5  6980  genpdf  6988  genipv  6989  genpelvl  6992  genpml  6997  genprndl  7001  genpassl  7004  addnqprllem  7007  addnqprl  7009  addlocprlemeqgt  7012  addlocprlemgt  7014  addlocprlem  7015  nqprl  7031  prmuloc  7046  mulnqprl  7048  addcomprg  7058  mulcomprg  7060  distrlem1prl  7062  distrlem4prl  7064  1idprl  7070  ltsopr  7076  ltexprlemm  7080  ltexprlemopl  7081  ltexprlemopu  7083  ltexprlemupu  7084  ltexprlemdisj  7086  ltexprlemloc  7087  ltexprlemfl  7089  ltexprlemrl  7090  ltexprlemfu  7091  ltexprlemru  7092  addcanprleml  7094  addcanprlemu  7095  recexprlemloc  7111  recexprlem1ssl  7113  recexprlem1ssu  7114  recexprlemss1l  7115  aptiprleml  7119  aptiprlemu  7120  caucvgprprlemopl  7177