Theorem prop 7650

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 7646	. . . 4 ⊢ P ⊆ (𝒫 Q × 𝒫 Q)
2	1	sseli 3220	. . 3 ⊢ (𝐴 ∈ P → 𝐴 ∈ (𝒫 Q × 𝒫 Q))
3		1st2nd2 6311	. . 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 4714  ‘cfv 5314  1^st c1st 6274  2^nd c2nd 6275  Qcnq 7455  Pcnp 7466

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 4201  ax-pow 4257  ax-pr 4292  ax-un 4521

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 3888  df-br 4083  df-opab 4145  df-mpt 4146  df-id 4381  df-xp 4722  df-rel 4723  df-cnv 4724  df-co 4725  df-dm 4726  df-rn 4727  df-iota 5274  df-fun 5316  df-fv 5322  df-1st 6276  df-2nd 6277  df-inp 7641

This theorem is referenced by:  elnp1st2nd  7651  0npr  7658  genpdf  7683  genipv  7684  genpelvl  7687  genpelvu  7688  genpml  7692  genpmu  7693  genprndl  7696  genprndu  7697  genpdisj  7698  genpassl  7699  genpassu  7700  addnqprl  7704  addnqpru  7705  addlocprlemeqgt  7707  addlocprlemgt  7709  addlocprlem  7710  addlocpr  7711  nqprl  7726  nqpru  7727  addnqprlemfl  7734  addnqprlemfu  7735  mulnqprl  7743  mulnqpru  7744  mullocprlem  7745  mullocpr  7746  mulnqprlemfl  7750  mulnqprlemfu  7751  addcomprg  7753  mulcomprg  7755  distrlem1prl  7757  distrlem1pru  7758  distrlem4prl  7759  distrlem4pru  7760  ltprordil  7764  1idprl  7765  1idpru  7766  ltpopr  7770  ltsopr  7771  ltaddpr  7772  ltexprlemm  7775  ltexprlemopl  7776  ltexprlemlol  7777  ltexprlemopu  7778  ltexprlemupu  7779  ltexprlemdisj  7781  ltexprlemloc  7782  ltexprlemfl  7784  ltexprlemrl  7785  ltexprlemfu  7786  ltexprlemru  7787  addcanprleml  7789  addcanprlemu  7790  prplnqu  7795  recexprlemm  7799  recexprlemdisj  7805  recexprlemloc  7806  recexprlem1ssl  7808  recexprlem1ssu  7809  recexprlemss1l  7810  recexprlemss1u  7811  aptiprleml  7814  aptiprlemu  7815  archpr  7818  cauappcvgprlemladdru  7831  cauappcvgprlemladdrl  7832  archrecpr  7839  caucvgprlemladdrl  7853  caucvgprprlemml  7869  caucvgprprlemmu  7870  caucvgprprlemopl  7872  suplocexprlemml  7891  suplocexprlemrl  7892  suplocexprlemmu  7893  suplocexprlemdisj  7895  suplocexprlemloc  7896  suplocexprlemex  7897  suplocexprlemub  7898