Theorem prop 7755

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 7751	. . . 4 |- P. C_ ( ~P Q. X. ~P Q. )
2	1	sseli 3224	. . 3 |- ( A e. P. -> A e. ( ~P Q. X. ~P Q. ) )
3		1st2nd2 6347	. . 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 1398   e. wcel 2202   ~Pcpw 3656   <.cop 3676   X. cxp 4729   ` cfv 5333   1stc1st 6310   2ndc2nd 6311   Q.cnq 7560   P.cnp 7571

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-un 4536

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-sbc 3033  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-mpt 4157  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-iota 5293  df-fun 5335  df-fv 5341  df-1st 6312  df-2nd 6313  df-inp 7746

This theorem is referenced by:  elnp1st2nd  7756  0npr  7763  genpdf  7788  genipv  7789  genpelvl  7792  genpelvu  7793  genpml  7797  genpmu  7798  genprndl  7801  genprndu  7802  genpdisj  7803  genpassl  7804  genpassu  7805  addnqprl  7809  addnqpru  7810  addlocprlemeqgt  7812  addlocprlemgt  7814  addlocprlem  7815  addlocpr  7816  nqprl  7831  nqpru  7832  addnqprlemfl  7839  addnqprlemfu  7840  mulnqprl  7848  mulnqpru  7849  mullocprlem  7850  mullocpr  7851  mulnqprlemfl  7855  mulnqprlemfu  7856  addcomprg  7858  mulcomprg  7860  distrlem1prl  7862  distrlem1pru  7863  distrlem4prl  7864  distrlem4pru  7865  ltprordil  7869  1idprl  7870  1idpru  7871  ltpopr  7875  ltsopr  7876  ltaddpr  7877  ltexprlemm  7880  ltexprlemopl  7881  ltexprlemlol  7882  ltexprlemopu  7883  ltexprlemupu  7884  ltexprlemdisj  7886  ltexprlemloc  7887  ltexprlemfl  7889  ltexprlemrl  7890  ltexprlemfu  7891  ltexprlemru  7892  addcanprleml  7894  addcanprlemu  7895  prplnqu  7900  recexprlemm  7904  recexprlemdisj  7910  recexprlemloc  7911  recexprlem1ssl  7913  recexprlem1ssu  7914  recexprlemss1l  7915  recexprlemss1u  7916  aptiprleml  7919  aptiprlemu  7920  archpr  7923  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  archrecpr  7944  caucvgprlemladdrl  7958  caucvgprprlemml  7974  caucvgprprlemmu  7975  caucvgprprlemopl  7977  suplocexprlemml  7996  suplocexprlemrl  7997  suplocexprlemmu  7998  suplocexprlemdisj  8000  suplocexprlemloc  8001  suplocexprlemex  8002  suplocexprlemub  8003