Theorem prop 6970

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 6966	. . . 4 ⊢ P ⊆ (𝒫 Q × 𝒫 Q)
2	1	sseli 3010	. . 3 ⊢ (𝐴 ∈ P → 𝐴 ∈ (𝒫 Q × 𝒫 Q))
3		1st2nd2 5895	. . 3 ⊢ (𝐴 ∈ (𝒫 Q × 𝒫 Q) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
4	2, 3	syl 14	. 2 ⊢ (𝐴 ∈ P → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
5		eleq1 2147	. . 3 ⊢ (𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ → (𝐴 ∈ P ↔ ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ P))
6	5	biimpcd 157	. 2 ⊢ (𝐴 ∈ P → (𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ → ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ P))
7	4, 6	mpd 13	1 ⊢ (𝐴 ∈ P → ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ P)

Syntax hints:   → wi 4   = wceq 1287   ∈ wcel 1436  𝒫 cpw 3414  ⟨cop 3433   × cxp 4407  ‘cfv 4977  1^st c1st 5859  2^nd c2nd 5860  Qcnq 6775  Pcnp 6786

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3930  ax-pow 3982  ax-pr 4008  ax-un 4232

This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-v 2617  df-sbc 2830  df-un 2992  df-in 2994  df-ss 3001  df-pw 3416  df-sn 3436  df-pr 3437  df-op 3439  df-uni 3636  df-br 3820  df-opab 3874  df-mpt 3875  df-id 4092  df-xp 4415  df-rel 4416  df-cnv 4417  df-co 4418  df-dm 4419  df-rn 4420  df-iota 4942  df-fun 4979  df-fv 4985  df-1st 5861  df-2nd 5862  df-inp 6961

This theorem is referenced by:  elnp1st2nd  6971  0npr  6978  genpdf  7003  genipv  7004  genpelvl  7007  genpelvu  7008  genpml  7012  genpmu  7013  genprndl  7016  genprndu  7017  genpdisj  7018  genpassl  7019  genpassu  7020  addnqprl  7024  addnqpru  7025  addlocprlemeqgt  7027  addlocprlemgt  7029  addlocprlem  7030  addlocpr  7031  nqprl  7046  nqpru  7047  addnqprlemfl  7054  addnqprlemfu  7055  mulnqprl  7063  mulnqpru  7064  mullocprlem  7065  mullocpr  7066  mulnqprlemfl  7070  mulnqprlemfu  7071  addcomprg  7073  mulcomprg  7075  distrlem1prl  7077  distrlem1pru  7078  distrlem4prl  7079  distrlem4pru  7080  ltprordil  7084  1idprl  7085  1idpru  7086  ltpopr  7090  ltsopr  7091  ltaddpr  7092  ltexprlemm  7095  ltexprlemopl  7096  ltexprlemlol  7097  ltexprlemopu  7098  ltexprlemupu  7099  ltexprlemdisj  7101  ltexprlemloc  7102  ltexprlemfl  7104  ltexprlemrl  7105  ltexprlemfu  7106  ltexprlemru  7107  addcanprleml  7109  addcanprlemu  7110  prplnqu  7115  recexprlemm  7119  recexprlemdisj  7125  recexprlemloc  7126  recexprlem1ssl  7128  recexprlem1ssu  7129  recexprlemss1l  7130  recexprlemss1u  7131  aptiprleml  7134  aptiprlemu  7135  archpr  7138  cauappcvgprlemladdru  7151  cauappcvgprlemladdrl  7152  archrecpr  7159  caucvgprlemladdrl  7173  caucvgprprlemml  7189  caucvgprprlemmu  7190  caucvgprprlemopl  7192