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

Theorem prop 6936
Description: A positive real is an ordered pair of a lower cut and an upper cut. (Contributed by Jim Kingdon, 27-Sep-2019.)
Assertion
Ref Expression
prop  |-  ( A  e.  P.  ->  <. ( 1st `  A ) ,  ( 2nd `  A
) >.  e.  P. )

Proof of Theorem prop
StepHypRef Expression
1 npsspw 6932 . . . 4  |-  P.  C_  ( ~P Q.  X.  ~P Q. )
21sseli 3006 . . 3  |-  ( A  e.  P.  ->  A  e.  ( ~P Q.  X.  ~P Q. ) )
3 1st2nd2 5879 . . 3  |-  ( A  e.  ( ~P Q.  X.  ~P Q. )  ->  A  =  <. ( 1st `  A ) ,  ( 2nd `  A )
>. )
42, 3syl 14 . 2  |-  ( A  e.  P.  ->  A  =  <. ( 1st `  A
) ,  ( 2nd `  A ) >. )
5 eleq1 2145 . . 3  |-  ( A  =  <. ( 1st `  A
) ,  ( 2nd `  A ) >.  ->  ( A  e.  P.  <->  <. ( 1st `  A ) ,  ( 2nd `  A )
>.  e.  P. ) )
65biimpcd 157 . 2  |-  ( A  e.  P.  ->  ( A  =  <. ( 1st `  A ) ,  ( 2nd `  A )
>.  ->  <. ( 1st `  A
) ,  ( 2nd `  A ) >.  e.  P. ) )
74, 6mpd 13 1  |-  ( A  e.  P.  ->  <. ( 1st `  A ) ,  ( 2nd `  A
) >.  e.  P. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1285    e. wcel 1434   ~Pcpw 3406   <.cop 3425    X. cxp 4398   ` cfv 4968   1stc1st 5843   2ndc2nd 5844   Q.cnq 6741   P.cnp 6752
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-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-pow 3974  ax-pr 3999  ax-un 4223
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2614  df-sbc 2827  df-un 2988  df-in 2990  df-ss 2997  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-br 3812  df-opab 3866  df-mpt 3867  df-id 4083  df-xp 4406  df-rel 4407  df-cnv 4408  df-co 4409  df-dm 4410  df-rn 4411  df-iota 4933  df-fun 4970  df-fv 4976  df-1st 5845  df-2nd 5846  df-inp 6927
This theorem is referenced by:  elnp1st2nd  6937  0npr  6944  genpdf  6969  genipv  6970  genpelvl  6973  genpelvu  6974  genpml  6978  genpmu  6979  genprndl  6982  genprndu  6983  genpdisj  6984  genpassl  6985  genpassu  6986  addnqprl  6990  addnqpru  6991  addlocprlemeqgt  6993  addlocprlemgt  6995  addlocprlem  6996  addlocpr  6997  nqprl  7012  nqpru  7013  addnqprlemfl  7020  addnqprlemfu  7021  mulnqprl  7029  mulnqpru  7030  mullocprlem  7031  mullocpr  7032  mulnqprlemfl  7036  mulnqprlemfu  7037  addcomprg  7039  mulcomprg  7041  distrlem1prl  7043  distrlem1pru  7044  distrlem4prl  7045  distrlem4pru  7046  ltprordil  7050  1idprl  7051  1idpru  7052  ltpopr  7056  ltsopr  7057  ltaddpr  7058  ltexprlemm  7061  ltexprlemopl  7062  ltexprlemlol  7063  ltexprlemopu  7064  ltexprlemupu  7065  ltexprlemdisj  7067  ltexprlemloc  7068  ltexprlemfl  7070  ltexprlemrl  7071  ltexprlemfu  7072  ltexprlemru  7073  addcanprleml  7075  addcanprlemu  7076  prplnqu  7081  recexprlemm  7085  recexprlemdisj  7091  recexprlemloc  7092  recexprlem1ssl  7094  recexprlem1ssu  7095  recexprlemss1l  7096  recexprlemss1u  7097  aptiprleml  7100  aptiprlemu  7101  archpr  7104  cauappcvgprlemladdru  7117  cauappcvgprlemladdrl  7118  archrecpr  7125  caucvgprlemladdrl  7139  caucvgprprlemml  7155  caucvgprprlemmu  7156  caucvgprprlemopl  7158
  Copyright terms: Public domain W3C validator