Theorem prop 7685

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

Step	Hyp	Ref	Expression
1		npsspw 7681	. . . 4 |- P. C_ ( ~P Q. X. ~P Q. )
2	1	sseli 3221	. . 3 |- ( A e. P. -> A e. ( ~P Q. X. ~P Q. ) )
3		1st2nd2 6333	. . 3 |- ( A e. ( ~P Q. X. ~P Q. ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
4	2, 3	syl 14	. 2 |- ( A e. P. -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
5		eleq1 2292	. . 3 |- ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. -> ( A e. P. <-> <. ( 1st ` A ) , ( 2nd ` A ) >. e. P. ) )
6	5	biimpcd 159	. 2 |- ( A e. P. -> ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. -> <. ( 1st ` A ) , ( 2nd ` A ) >. e. P. ) )
7	4, 6	mpd 13	1 |- ( A e. P. -> <. ( 1st ` A ) , ( 2nd ` A ) >. e. P. )

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200   ~Pcpw 3650   <.cop 3670   X. cxp 4721   ` cfv 5324   1stc1st 6296   2ndc2nd 6297   Q.cnq 7490   P.cnp 7501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297  ax-un 4528

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-sbc 3030  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-mpt 4150  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-rn 4734  df-iota 5284  df-fun 5326  df-fv 5332  df-1st 6298  df-2nd 6299  df-inp 7676

This theorem is referenced by:  elnp1st2nd  7686  0npr  7693  genpdf  7718  genipv  7719  genpelvl  7722  genpelvu  7723  genpml  7727  genpmu  7728  genprndl  7731  genprndu  7732  genpdisj  7733  genpassl  7734  genpassu  7735  addnqprl  7739  addnqpru  7740  addlocprlemeqgt  7742  addlocprlemgt  7744  addlocprlem  7745  addlocpr  7746  nqprl  7761  nqpru  7762  addnqprlemfl  7769  addnqprlemfu  7770  mulnqprl  7778  mulnqpru  7779  mullocprlem  7780  mullocpr  7781  mulnqprlemfl  7785  mulnqprlemfu  7786  addcomprg  7788  mulcomprg  7790  distrlem1prl  7792  distrlem1pru  7793  distrlem4prl  7794  distrlem4pru  7795  ltprordil  7799  1idprl  7800  1idpru  7801  ltpopr  7805  ltsopr  7806  ltaddpr  7807  ltexprlemm  7810  ltexprlemopl  7811  ltexprlemlol  7812  ltexprlemopu  7813  ltexprlemupu  7814  ltexprlemdisj  7816  ltexprlemloc  7817  ltexprlemfl  7819  ltexprlemrl  7820  ltexprlemfu  7821  ltexprlemru  7822  addcanprleml  7824  addcanprlemu  7825  prplnqu  7830  recexprlemm  7834  recexprlemdisj  7840  recexprlemloc  7841  recexprlem1ssl  7843  recexprlem1ssu  7844  recexprlemss1l  7845  recexprlemss1u  7846  aptiprleml  7849  aptiprlemu  7850  archpr  7853  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  archrecpr  7874  caucvgprlemladdrl  7888  caucvgprprlemml  7904  caucvgprprlemmu  7905  caucvgprprlemopl  7907  suplocexprlemml  7926  suplocexprlemrl  7927  suplocexprlemmu  7928  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemex  7932  suplocexprlemub  7933