Theorem prop 7623

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 7619	. . . 4 |- P. C_ ( ~P Q. X. ~P Q. )
2	1	sseli 3197	. . 3 |- ( A e. P. -> A e. ( ~P Q. X. ~P Q. ) )
3		1st2nd2 6284	. . 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 2270	. . 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 1373   e. wcel 2178   ~Pcpw 3626   <.cop 3646   X. cxp 4691   ` cfv 5290   1stc1st 6247   2ndc2nd 6248   Q.cnq 7428   P.cnp 7439

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2180  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269  ax-un 4498

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-v 2778  df-sbc 3006  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-opab 4122  df-mpt 4123  df-id 4358  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-rn 4704  df-iota 5251  df-fun 5292  df-fv 5298  df-1st 6249  df-2nd 6250  df-inp 7614

This theorem is referenced by:  elnp1st2nd  7624  0npr  7631  genpdf  7656  genipv  7657  genpelvl  7660  genpelvu  7661  genpml  7665  genpmu  7666  genprndl  7669  genprndu  7670  genpdisj  7671  genpassl  7672  genpassu  7673  addnqprl  7677  addnqpru  7678  addlocprlemeqgt  7680  addlocprlemgt  7682  addlocprlem  7683  addlocpr  7684  nqprl  7699  nqpru  7700  addnqprlemfl  7707  addnqprlemfu  7708  mulnqprl  7716  mulnqpru  7717  mullocprlem  7718  mullocpr  7719  mulnqprlemfl  7723  mulnqprlemfu  7724  addcomprg  7726  mulcomprg  7728  distrlem1prl  7730  distrlem1pru  7731  distrlem4prl  7732  distrlem4pru  7733  ltprordil  7737  1idprl  7738  1idpru  7739  ltpopr  7743  ltsopr  7744  ltaddpr  7745  ltexprlemm  7748  ltexprlemopl  7749  ltexprlemlol  7750  ltexprlemopu  7751  ltexprlemupu  7752  ltexprlemdisj  7754  ltexprlemloc  7755  ltexprlemfl  7757  ltexprlemrl  7758  ltexprlemfu  7759  ltexprlemru  7760  addcanprleml  7762  addcanprlemu  7763  prplnqu  7768  recexprlemm  7772  recexprlemdisj  7778  recexprlemloc  7779  recexprlem1ssl  7781  recexprlem1ssu  7782  recexprlemss1l  7783  recexprlemss1u  7784  aptiprleml  7787  aptiprlemu  7788  archpr  7791  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  archrecpr  7812  caucvgprlemladdrl  7826  caucvgprprlemml  7842  caucvgprprlemmu  7843  caucvgprprlemopl  7845  suplocexprlemml  7864  suplocexprlemrl  7865  suplocexprlemmu  7866  suplocexprlemdisj  7868  suplocexprlemloc  7869  suplocexprlemex  7870  suplocexprlemub  7871