Theorem prop 7694

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 7690	. . . 4 |- P. C_ ( ~P Q. X. ~P Q. )
2	1	sseli 3223	. . 3 |- ( A e. P. -> A e. ( ~P Q. X. ~P Q. ) )
3		1st2nd2 6337	. . 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 2294	. . 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 1397   e. wcel 2202   ~Pcpw 3652   <.cop 3672   X. cxp 4723   ` cfv 5326   1stc1st 6300   2ndc2nd 6301   Q.cnq 7499   P.cnp 7510

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-mpt 4152  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-iota 5286  df-fun 5328  df-fv 5334  df-1st 6302  df-2nd 6303  df-inp 7685

This theorem is referenced by:  elnp1st2nd  7695  0npr  7702  genpdf  7727  genipv  7728  genpelvl  7731  genpelvu  7732  genpml  7736  genpmu  7737  genprndl  7740  genprndu  7741  genpdisj  7742  genpassl  7743  genpassu  7744  addnqprl  7748  addnqpru  7749  addlocprlemeqgt  7751  addlocprlemgt  7753  addlocprlem  7754  addlocpr  7755  nqprl  7770  nqpru  7771  addnqprlemfl  7778  addnqprlemfu  7779  mulnqprl  7787  mulnqpru  7788  mullocprlem  7789  mullocpr  7790  mulnqprlemfl  7794  mulnqprlemfu  7795  addcomprg  7797  mulcomprg  7799  distrlem1prl  7801  distrlem1pru  7802  distrlem4prl  7803  distrlem4pru  7804  ltprordil  7808  1idprl  7809  1idpru  7810  ltpopr  7814  ltsopr  7815  ltaddpr  7816  ltexprlemm  7819  ltexprlemopl  7820  ltexprlemlol  7821  ltexprlemopu  7822  ltexprlemupu  7823  ltexprlemdisj  7825  ltexprlemloc  7826  ltexprlemfl  7828  ltexprlemrl  7829  ltexprlemfu  7830  ltexprlemru  7831  addcanprleml  7833  addcanprlemu  7834  prplnqu  7839  recexprlemm  7843  recexprlemdisj  7849  recexprlemloc  7850  recexprlem1ssl  7852  recexprlem1ssu  7853  recexprlemss1l  7854  recexprlemss1u  7855  aptiprleml  7858  aptiprlemu  7859  archpr  7862  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  archrecpr  7883  caucvgprlemladdrl  7897  caucvgprprlemml  7913  caucvgprprlemmu  7914  caucvgprprlemopl  7916  suplocexprlemml  7935  suplocexprlemrl  7936  suplocexprlemmu  7937  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemex  7941  suplocexprlemub  7942