MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prcdnq Unicode version

Theorem prcdnq 8619
Description: A positive real is closed downwards under the positive fractions. Definition 9-3.1 (ii) of [Gleason] p. 121. (Contributed by NM, 25-Feb-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
Assertion
Ref Expression
prcdnq  |-  ( ( A  e.  P.  /\  B  e.  A )  ->  ( C  <Q  B  ->  C  e.  A )
)

Proof of Theorem prcdnq
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrelnq 8552 . . . . . . 7  |-  <Q  C_  ( Q.  X.  Q. )
2 relxp 4796 . . . . . . 7  |-  Rel  ( Q.  X.  Q. )
3 relss 4777 . . . . . . 7  |-  (  <Q  C_  ( Q.  X.  Q. )  ->  ( Rel  ( Q.  X.  Q. )  ->  Rel  <Q  ) )
41, 2, 3mp2 17 . . . . . 6  |-  Rel  <Q
54brrelexi 4731 . . . . 5  |-  ( C 
<Q  B  ->  C  e. 
_V )
6 eleq1 2345 . . . . . . . . 9  |-  ( x  =  B  ->  (
x  e.  A  <->  B  e.  A ) )
76anbi2d 684 . . . . . . . 8  |-  ( x  =  B  ->  (
( A  e.  P.  /\  x  e.  A )  <-> 
( A  e.  P.  /\  B  e.  A ) ) )
8 breq2 4029 . . . . . . . 8  |-  ( x  =  B  ->  (
y  <Q  x  <->  y  <Q  B ) )
97, 8anbi12d 691 . . . . . . 7  |-  ( x  =  B  ->  (
( ( A  e. 
P.  /\  x  e.  A )  /\  y  <Q  x )  <->  ( ( A  e.  P.  /\  B  e.  A )  /\  y  <Q  B ) ) )
109imbi1d 308 . . . . . 6  |-  ( x  =  B  ->  (
( ( ( A  e.  P.  /\  x  e.  A )  /\  y  <Q  x )  ->  y  e.  A )  <->  ( (
( A  e.  P.  /\  B  e.  A )  /\  y  <Q  B )  ->  y  e.  A
) ) )
11 breq1 4028 . . . . . . . 8  |-  ( y  =  C  ->  (
y  <Q  B  <->  C  <Q  B ) )
1211anbi2d 684 . . . . . . 7  |-  ( y  =  C  ->  (
( ( A  e. 
P.  /\  B  e.  A )  /\  y  <Q  B )  <->  ( ( A  e.  P.  /\  B  e.  A )  /\  C  <Q  B ) ) )
13 eleq1 2345 . . . . . . 7  |-  ( y  =  C  ->  (
y  e.  A  <->  C  e.  A ) )
1412, 13imbi12d 311 . . . . . 6  |-  ( y  =  C  ->  (
( ( ( A  e.  P.  /\  B  e.  A )  /\  y  <Q  B )  ->  y  e.  A )  <->  ( (
( A  e.  P.  /\  B  e.  A )  /\  C  <Q  B )  ->  C  e.  A
) ) )
15 elnpi 8614 . . . . . . . . . . 11  |-  ( A  e.  P.  <->  ( ( A  e.  _V  /\  (/)  C.  A  /\  A  C.  Q. )  /\  A. x  e.  A  ( A. y ( y 
<Q  x  ->  y  e.  A )  /\  E. y  e.  A  x  <Q  y ) ) )
1615simprbi 450 . . . . . . . . . 10  |-  ( A  e.  P.  ->  A. x  e.  A  ( A. y ( y  <Q  x  ->  y  e.  A
)  /\  E. y  e.  A  x  <Q  y ) )
1716r19.21bi 2643 . . . . . . . . 9  |-  ( ( A  e.  P.  /\  x  e.  A )  ->  ( A. y ( y  <Q  x  ->  y  e.  A )  /\  E. y  e.  A  x 
<Q  y ) )
1817simpld 445 . . . . . . . 8  |-  ( ( A  e.  P.  /\  x  e.  A )  ->  A. y ( y 
<Q  x  ->  y  e.  A ) )
191819.21bi 1796 . . . . . . 7  |-  ( ( A  e.  P.  /\  x  e.  A )  ->  ( y  <Q  x  ->  y  e.  A ) )
2019imp 418 . . . . . 6  |-  ( ( ( A  e.  P.  /\  x  e.  A )  /\  y  <Q  x
)  ->  y  e.  A )
2110, 14, 20vtocl2g 2849 . . . . 5  |-  ( ( B  e.  A  /\  C  e.  _V )  ->  ( ( ( A  e.  P.  /\  B  e.  A )  /\  C  <Q  B )  ->  C  e.  A ) )
225, 21sylan2 460 . . . 4  |-  ( ( B  e.  A  /\  C  <Q  B )  -> 
( ( ( A  e.  P.  /\  B  e.  A )  /\  C  <Q  B )  ->  C  e.  A ) )
2322adantll 694 . . 3  |-  ( ( ( A  e.  P.  /\  B  e.  A )  /\  C  <Q  B )  ->  ( ( ( A  e.  P.  /\  B  e.  A )  /\  C  <Q  B )  ->  C  e.  A
) )
2423pm2.43i 43 . 2  |-  ( ( ( A  e.  P.  /\  B  e.  A )  /\  C  <Q  B )  ->  C  e.  A
)
2524ex 423 1  |-  ( ( A  e.  P.  /\  B  e.  A )  ->  ( C  <Q  B  ->  C  e.  A )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934   A.wal 1529    = wceq 1625    e. wcel 1686   A.wral 2545   E.wrex 2546   _Vcvv 2790    C_ wss 3154    C. wpss 3155   (/)c0 3457   class class class wbr 4025    X. cxp 4689   Rel wrel 4696   Q.cnq 8476    <Q cltq 8482   P.cnp 8483
This theorem is referenced by:  prub  8620  addclprlem1  8642  mulclprlem  8645  distrlem4pr  8652  1idpr  8655  psslinpr  8657  prlem934  8659  ltaddpr  8660  ltexprlem2  8663  ltexprlem3  8664  ltexprlem6  8667  prlem936  8673  reclem2pr  8674  suplem1pr  8678
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026  df-opab 4080  df-xp 4697  df-rel 4698  df-ltnq 8544  df-np 8607
  Copyright terms: Public domain W3C validator