Theorem elprnql 7447

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	|- ( ( <. L , U >. e. P. /\ B e. L ) -> B e. Q. )

Proof of Theorem elprnql

Step	Hyp	Ref	Expression
1		prssnql 7445	. 2 |- ( <. L , U >. e. P. -> L C_ Q. )
2	1	sselda 3148	1 |- ( ( <. L , U >. e. P. /\ B e. L ) -> B e. Q. )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2142   <.cop 3587   Q.cnq 7246   P.cnp 7257

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 610  ax-in2 611  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-13 2144  ax-14 2145  ax-ext 2153  ax-coll 4105  ax-sep 4108  ax-pow 4161  ax-pr 4195  ax-un 4419  ax-iinf 4573

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ral 2454  df-rex 2455  df-reu 2456  df-rab 2458  df-v 2733  df-sbc 2957  df-csb 3051  df-dif 3124  df-un 3126  df-in 3128  df-ss 3135  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-int 3833  df-iun 3876  df-br 3991  df-opab 4052  df-mpt 4053  df-id 4279  df-iom 4576  df-xp 4618  df-rel 4619  df-cnv 4620  df-co 4621  df-dm 4622  df-rn 4623  df-res 4624  df-ima 4625  df-iota 5162  df-fun 5202  df-fn 5203  df-f 5204  df-f1 5205  df-fo 5206  df-f1o 5207  df-fv 5208  df-qs 6523  df-ni 7270  df-nqqs 7314  df-inp 7432

This theorem is referenced by:  prubl  7452  prnmaxl  7454  prarloclemlt  7459  prarloclemlo  7460  prarloclem5  7466  genpdf  7474  genipv  7475  genpelvl  7478  genpml  7483  genprndl  7487  genpassl  7490  addnqprllem  7493  addnqprl  7495  addlocprlemeqgt  7498  addlocprlemgt  7500  addlocprlem  7501  nqprl  7517  prmuloc  7532  mulnqprl  7534  addcomprg  7544  mulcomprg  7546  distrlem1prl  7548  distrlem4prl  7550  1idprl  7556  ltsopr  7562  ltexprlemm  7566  ltexprlemopl  7567  ltexprlemopu  7569  ltexprlemupu  7570  ltexprlemdisj  7572  ltexprlemloc  7573  ltexprlemfl  7575  ltexprlemrl  7576  ltexprlemfu  7577  ltexprlemru  7578  addcanprleml  7580  addcanprlemu  7581  recexprlemloc  7597  recexprlem1ssl  7599  recexprlem1ssu  7600  recexprlemss1l  7601  aptiprleml  7605  aptiprlemu  7606  caucvgprprlemopl  7663  suplocexprlemex  7688