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

Theorem prcunqu 7418
Description: An upper cut is closed upwards under the positive fractions. (Contributed by Jim Kingdon, 25-Nov-2019.)
Assertion
Ref Expression
prcunqu  |-  ( (
<. L ,  U >.  e. 
P.  /\  C  e.  U )  ->  ( C  <Q  B  ->  B  e.  U ) )

Proof of Theorem prcunqu
Dummy variables  b  c are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrelnq 7298 . . . . . 6  |-  <Q  C_  ( Q.  X.  Q. )
21brel 4651 . . . . 5  |-  ( C 
<Q  B  ->  ( C  e.  Q.  /\  B  e.  Q. ) )
32simprd 113 . . . 4  |-  ( C 
<Q  B  ->  B  e. 
Q. )
43adantl 275 . . 3  |-  ( ( ( <. L ,  U >.  e.  P.  /\  C  e.  U )  /\  C  <Q  B )  ->  B  e.  Q. )
5 breq2 3981 . . . . . . 7  |-  ( b  =  B  ->  ( C  <Q  b  <->  C  <Q  B ) )
6 eleq1 2227 . . . . . . 7  |-  ( b  =  B  ->  (
b  e.  U  <->  B  e.  U ) )
75, 6imbi12d 233 . . . . . 6  |-  ( b  =  B  ->  (
( C  <Q  b  ->  b  e.  U )  <-> 
( C  <Q  B  ->  B  e.  U )
) )
87imbi2d 229 . . . . 5  |-  ( b  =  B  ->  (
( ( <. L ,  U >.  e.  P.  /\  C  e.  U )  ->  ( C  <Q  b  ->  b  e.  U ) )  <->  ( ( <. L ,  U >.  e. 
P.  /\  C  e.  U )  ->  ( C  <Q  B  ->  B  e.  U ) ) ) )
91brel 4651 . . . . . . . 8  |-  ( C 
<Q  b  ->  ( C  e.  Q.  /\  b  e.  Q. ) )
10 an42 577 . . . . . . . . 9  |-  ( ( ( C  e.  Q.  /\  b  e.  Q. )  /\  ( C  e.  U  /\  <. L ,  U >.  e.  P. ) )  <-> 
( ( C  e. 
Q.  /\  C  e.  U )  /\  ( <. L ,  U >.  e. 
P.  /\  b  e.  Q. ) ) )
11 breq1 3980 . . . . . . . . . . . . . . . 16  |-  ( c  =  C  ->  (
c  <Q  b  <->  C  <Q  b ) )
12 eleq1 2227 . . . . . . . . . . . . . . . 16  |-  ( c  =  C  ->  (
c  e.  U  <->  C  e.  U ) )
1311, 12anbi12d 465 . . . . . . . . . . . . . . 15  |-  ( c  =  C  ->  (
( c  <Q  b  /\  c  e.  U
)  <->  ( C  <Q  b  /\  C  e.  U
) ) )
1413rspcev 2826 . . . . . . . . . . . . . 14  |-  ( ( C  e.  Q.  /\  ( C  <Q  b  /\  C  e.  U )
)  ->  E. c  e.  Q.  ( c  <Q 
b  /\  c  e.  U ) )
15 elinp 7407 . . . . . . . . . . . . . . . 16  |-  ( <. L ,  U >.  e. 
P. 
<->  ( ( ( L 
C_  Q.  /\  U  C_  Q. )  /\  ( E. c  e.  Q.  c  e.  L  /\  E. b  e.  Q.  b  e.  U ) )  /\  ( ( A. c  e.  Q.  ( c  e.  L  <->  E. b  e.  Q.  ( c  <Q  b  /\  b  e.  L
) )  /\  A. b  e.  Q.  (
b  e.  U  <->  E. c  e.  Q.  ( c  <Q 
b  /\  c  e.  U ) ) )  /\  A. c  e. 
Q.  -.  ( c  e.  L  /\  c  e.  U )  /\  A. c  e.  Q.  A. b  e.  Q.  ( c  <Q 
b  ->  ( c  e.  L  \/  b  e.  U ) ) ) ) )
16 simpr1r 1044 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( L  C_  Q.  /\  U  C_  Q. )  /\  ( E. c  e.  Q.  c  e.  L  /\  E. b  e.  Q.  b  e.  U )
)  /\  ( ( A. c  e.  Q.  ( c  e.  L  <->  E. b  e.  Q.  (
c  <Q  b  /\  b  e.  L ) )  /\  A. b  e.  Q.  (
b  e.  U  <->  E. c  e.  Q.  ( c  <Q 
b  /\  c  e.  U ) ) )  /\  A. c  e. 
Q.  -.  ( c  e.  L  /\  c  e.  U )  /\  A. c  e.  Q.  A. b  e.  Q.  ( c  <Q 
b  ->  ( c  e.  L  \/  b  e.  U ) ) ) )  ->  A. b  e.  Q.  ( b  e.  U  <->  E. c  e.  Q.  ( c  <Q  b  /\  c  e.  U
) ) )
1715, 16sylbi 120 . . . . . . . . . . . . . . 15  |-  ( <. L ,  U >.  e. 
P.  ->  A. b  e.  Q.  ( b  e.  U  <->  E. c  e.  Q.  (
c  <Q  b  /\  c  e.  U ) ) )
1817r19.21bi 2552 . . . . . . . . . . . . . 14  |-  ( (
<. L ,  U >.  e. 
P.  /\  b  e.  Q. )  ->  ( b  e.  U  <->  E. c  e.  Q.  ( c  <Q 
b  /\  c  e.  U ) ) )
1914, 18syl5ibrcom 156 . . . . . . . . . . . . 13  |-  ( ( C  e.  Q.  /\  ( C  <Q  b  /\  C  e.  U )
)  ->  ( ( <. L ,  U >.  e. 
P.  /\  b  e.  Q. )  ->  b  e.  U ) )
20193impb 1188 . . . . . . . . . . . 12  |-  ( ( C  e.  Q.  /\  C  <Q  b  /\  C  e.  U )  ->  (
( <. L ,  U >.  e.  P.  /\  b  e.  Q. )  ->  b  e.  U ) )
21203com12 1196 . . . . . . . . . . 11  |-  ( ( C  <Q  b  /\  C  e.  Q.  /\  C  e.  U )  ->  (
( <. L ,  U >.  e.  P.  /\  b  e.  Q. )  ->  b  e.  U ) )
22213expib 1195 . . . . . . . . . 10  |-  ( C 
<Q  b  ->  ( ( C  e.  Q.  /\  C  e.  U )  ->  ( ( <. L ,  U >.  e.  P.  /\  b  e.  Q. )  ->  b  e.  U ) ) )
2322impd 252 . . . . . . . . 9  |-  ( C 
<Q  b  ->  ( ( ( C  e.  Q.  /\  C  e.  U )  /\  ( <. L ,  U >.  e.  P.  /\  b  e.  Q. )
)  ->  b  e.  U ) )
2410, 23syl5bi 151 . . . . . . . 8  |-  ( C 
<Q  b  ->  ( ( ( C  e.  Q.  /\  b  e.  Q. )  /\  ( C  e.  U  /\  <. L ,  U >.  e.  P. ) )  ->  b  e.  U
) )
259, 24mpand 426 . . . . . . 7  |-  ( C 
<Q  b  ->  ( ( C  e.  U  /\  <. L ,  U >.  e. 
P. )  ->  b  e.  U ) )
2625com12 30 . . . . . 6  |-  ( ( C  e.  U  /\  <. L ,  U >.  e. 
P. )  ->  ( C  <Q  b  ->  b  e.  U ) )
2726ancoms 266 . . . . 5  |-  ( (
<. L ,  U >.  e. 
P.  /\  C  e.  U )  ->  ( C  <Q  b  ->  b  e.  U ) )
288, 27vtoclg 2782 . . . 4  |-  ( B  e.  Q.  ->  (
( <. L ,  U >.  e.  P.  /\  C  e.  U )  ->  ( C  <Q  B  ->  B  e.  U ) ) )
2928impd 252 . . 3  |-  ( B  e.  Q.  ->  (
( ( <. L ,  U >.  e.  P.  /\  C  e.  U )  /\  C  <Q  B )  ->  B  e.  U
) )
304, 29mpcom 36 . 2  |-  ( ( ( <. L ,  U >.  e.  P.  /\  C  e.  U )  /\  C  <Q  B )  ->  B  e.  U )
3130ex 114 1  |-  ( (
<. L ,  U >.  e. 
P.  /\  C  e.  U )  ->  ( C  <Q  B  ->  B  e.  U ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 698    /\ w3a 967    = wceq 1342    e. wcel 2135   A.wral 2442   E.wrex 2443    C_ wss 3112   <.cop 3574   class class class wbr 3977   Q.cnq 7213    <Q cltq 7218   P.cnp 7224
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 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-coll 4092  ax-sep 4095  ax-pow 4148  ax-pr 4182  ax-un 4406  ax-iinf 4560
This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-rex 2448  df-reu 2449  df-rab 2451  df-v 2724  df-sbc 2948  df-csb 3042  df-dif 3114  df-un 3116  df-in 3118  df-ss 3125  df-pw 3556  df-sn 3577  df-pr 3578  df-op 3580  df-uni 3785  df-int 3820  df-iun 3863  df-br 3978  df-opab 4039  df-mpt 4040  df-id 4266  df-iom 4563  df-xp 4605  df-rel 4606  df-cnv 4607  df-co 4608  df-dm 4609  df-rn 4610  df-res 4611  df-ima 4612  df-iota 5148  df-fun 5185  df-fn 5186  df-f 5187  df-f1 5188  df-fo 5189  df-f1o 5190  df-fv 5191  df-qs 6499  df-ni 7237  df-nqqs 7281  df-ltnqqs 7286  df-inp 7399
This theorem is referenced by:  prarloc  7436  prarloc2  7437  addnqprulem  7461  nqpru  7485  prmuloc2  7500  mulnqpru  7502  distrlem4pru  7518  1idpru  7524  ltexprlemm  7533  ltexprlemupu  7537  ltexprlemrl  7543  ltexprlemfu  7544  ltexprlemru  7545  aptiprlemu  7573  suplocexprlemdisj  7653  suplocexprlemub  7656
  Copyright terms: Public domain W3C validator