Theorem prop 7688

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 7684	. . . 4 ⊢ P ⊆ (𝒫 Q × 𝒫 Q)
2	1	sseli 3221	. . 3 ⊢ (𝐴 ∈ P → 𝐴 ∈ (𝒫 Q × 𝒫 Q))
3		1st2nd2 6333	. . 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 3650  ⟨cop 3670   × cxp 4721  ‘cfv 5324  1^st c1st 6296  2^nd c2nd 6297  Qcnq 7493  Pcnp 7504

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 4205  ax-pow 4262  ax-pr 4297  ax-un 4528

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 2802  df-sbc 3030  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-mpt 4150  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-rn 4734  df-iota 5284  df-fun 5326  df-fv 5332  df-1st 6298  df-2nd 6299  df-inp 7679

This theorem is referenced by:  elnp1st2nd  7689  0npr  7696  genpdf  7721  genipv  7722  genpelvl  7725  genpelvu  7726  genpml  7730  genpmu  7731  genprndl  7734  genprndu  7735  genpdisj  7736  genpassl  7737  genpassu  7738  addnqprl  7742  addnqpru  7743  addlocprlemeqgt  7745  addlocprlemgt  7747  addlocprlem  7748  addlocpr  7749  nqprl  7764  nqpru  7765  addnqprlemfl  7772  addnqprlemfu  7773  mulnqprl  7781  mulnqpru  7782  mullocprlem  7783  mullocpr  7784  mulnqprlemfl  7788  mulnqprlemfu  7789  addcomprg  7791  mulcomprg  7793  distrlem1prl  7795  distrlem1pru  7796  distrlem4prl  7797  distrlem4pru  7798  ltprordil  7802  1idprl  7803  1idpru  7804  ltpopr  7808  ltsopr  7809  ltaddpr  7810  ltexprlemm  7813  ltexprlemopl  7814  ltexprlemlol  7815  ltexprlemopu  7816  ltexprlemupu  7817  ltexprlemdisj  7819  ltexprlemloc  7820  ltexprlemfl  7822  ltexprlemrl  7823  ltexprlemfu  7824  ltexprlemru  7825  addcanprleml  7827  addcanprlemu  7828  prplnqu  7833  recexprlemm  7837  recexprlemdisj  7843  recexprlemloc  7844  recexprlem1ssl  7846  recexprlem1ssu  7847  recexprlemss1l  7848  recexprlemss1u  7849  aptiprleml  7852  aptiprlemu  7853  archpr  7856  cauappcvgprlemladdru  7869  cauappcvgprlemladdrl  7870  archrecpr  7877  caucvgprlemladdrl  7891  caucvgprprlemml  7907  caucvgprprlemmu  7908  caucvgprprlemopl  7910  suplocexprlemml  7929  suplocexprlemrl  7930  suplocexprlemmu  7931  suplocexprlemdisj  7933  suplocexprlemloc  7934  suplocexprlemex  7935  suplocexprlemub  7936