Theorem prop 7678

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	⊢ (𝐴 ∈ P → ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ P)

Proof of Theorem prop

Step	Hyp	Ref	Expression
1		npsspw 7674	. . . 4 ⊢ P ⊆ (𝒫 Q × 𝒫 Q)
2	1	sseli 3220	. . 3 ⊢ (𝐴 ∈ P → 𝐴 ∈ (𝒫 Q × 𝒫 Q))
3		1st2nd2 6330	. . 3 ⊢ (𝐴 ∈ (𝒫 Q × 𝒫 Q) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
4	2, 3	syl 14	. 2 ⊢ (𝐴 ∈ P → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
5		eleq1 2292	. . 3 ⊢ (𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ → (𝐴 ∈ P ↔ ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ P))
6	5	biimpcd 159	. 2 ⊢ (𝐴 ∈ P → (𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ → ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ P))
7	4, 6	mpd 13	1 ⊢ (𝐴 ∈ P → ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ P)

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  𝒫 cpw 3649  ⟨cop 3669   × cxp 4718  ‘cfv 5321  1^st c1st 6293  2^nd c2nd 6294  Qcnq 7483  Pcnp 7494

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 4202  ax-pow 4259  ax-pr 4294  ax-un 4525

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 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-opab 4146  df-mpt 4147  df-id 4385  df-xp 4726  df-rel 4727  df-cnv 4728  df-co 4729  df-dm 4730  df-rn 4731  df-iota 5281  df-fun 5323  df-fv 5329  df-1st 6295  df-2nd 6296  df-inp 7669

This theorem is referenced by:  elnp1st2nd  7679  0npr  7686  genpdf  7711  genipv  7712  genpelvl  7715  genpelvu  7716  genpml  7720  genpmu  7721  genprndl  7724  genprndu  7725  genpdisj  7726  genpassl  7727  genpassu  7728  addnqprl  7732  addnqpru  7733  addlocprlemeqgt  7735  addlocprlemgt  7737  addlocprlem  7738  addlocpr  7739  nqprl  7754  nqpru  7755  addnqprlemfl  7762  addnqprlemfu  7763  mulnqprl  7771  mulnqpru  7772  mullocprlem  7773  mullocpr  7774  mulnqprlemfl  7778  mulnqprlemfu  7779  addcomprg  7781  mulcomprg  7783  distrlem1prl  7785  distrlem1pru  7786  distrlem4prl  7787  distrlem4pru  7788  ltprordil  7792  1idprl  7793  1idpru  7794  ltpopr  7798  ltsopr  7799  ltaddpr  7800  ltexprlemm  7803  ltexprlemopl  7804  ltexprlemlol  7805  ltexprlemopu  7806  ltexprlemupu  7807  ltexprlemdisj  7809  ltexprlemloc  7810  ltexprlemfl  7812  ltexprlemrl  7813  ltexprlemfu  7814  ltexprlemru  7815  addcanprleml  7817  addcanprlemu  7818  prplnqu  7823  recexprlemm  7827  recexprlemdisj  7833  recexprlemloc  7834  recexprlem1ssl  7836  recexprlem1ssu  7837  recexprlemss1l  7838  recexprlemss1u  7839  aptiprleml  7842  aptiprlemu  7843  archpr  7846  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  archrecpr  7867  caucvgprlemladdrl  7881  caucvgprprlemml  7897  caucvgprprlemmu  7898  caucvgprprlemopl  7900  suplocexprlemml  7919  suplocexprlemrl  7920  suplocexprlemmu  7921  suplocexprlemdisj  7923  suplocexprlemloc  7924  suplocexprlemex  7925  suplocexprlemub  7926