Theorem prop 7790

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 7786	. . . 4 |- P. C_ ( ~P Q. X. ~P Q. )
2	1	sseli 3234	. . 3 |- ( A e. P. -> A e. ( ~P Q. X. ~P Q. ) )
3		1st2nd2 6369	. . 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 2295	. . 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 2203   ~Pcpw 3669   <.cop 3692   X. cxp 4747   ` cfv 5352   1stc1st 6332   2ndc2nd 6333   Q.cnq 7595   P.cnp 7606

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 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-un 4554

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-sbc 3043  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-mpt 4173  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-rn 4760  df-iota 5312  df-fun 5354  df-fv 5360  df-1st 6334  df-2nd 6335  df-inp 7781

This theorem is referenced by:  elnp1st2nd  7791  0npr  7798  genpdf  7823  genipv  7824  genpelvl  7827  genpelvu  7828  genpml  7832  genpmu  7833  genprndl  7836  genprndu  7837  genpdisj  7838  genpassl  7839  genpassu  7840  addnqprl  7844  addnqpru  7845  addlocprlemeqgt  7847  addlocprlemgt  7849  addlocprlem  7850  addlocpr  7851  nqprl  7866  nqpru  7867  addnqprlemfl  7874  addnqprlemfu  7875  mulnqprl  7883  mulnqpru  7884  mullocprlem  7885  mullocpr  7886  mulnqprlemfl  7890  mulnqprlemfu  7891  addcomprg  7893  mulcomprg  7895  distrlem1prl  7897  distrlem1pru  7898  distrlem4prl  7899  distrlem4pru  7900  ltprordil  7904  1idprl  7905  1idpru  7906  ltpopr  7910  ltsopr  7911  ltaddpr  7912  ltexprlemm  7915  ltexprlemopl  7916  ltexprlemlol  7917  ltexprlemopu  7918  ltexprlemupu  7919  ltexprlemdisj  7921  ltexprlemloc  7922  ltexprlemfl  7924  ltexprlemrl  7925  ltexprlemfu  7926  ltexprlemru  7927  addcanprleml  7929  addcanprlemu  7930  prplnqu  7935  recexprlemm  7939  recexprlemdisj  7945  recexprlemloc  7946  recexprlem1ssl  7948  recexprlem1ssu  7949  recexprlemss1l  7950  recexprlemss1u  7951  aptiprleml  7954  aptiprlemu  7955  archpr  7958  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  archrecpr  7979  caucvgprlemladdrl  7993  caucvgprprlemml  8009  caucvgprprlemmu  8010  caucvgprprlemopl  8012  suplocexprlemml  8031  suplocexprlemrl  8032  suplocexprlemmu  8033  suplocexprlemdisj  8035  suplocexprlemloc  8036  suplocexprlemex  8037  suplocexprlemub  8038