Theorem prop 7738

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 7734	. . . 4 ⊢ P ⊆ (𝒫 Q × 𝒫 Q)
2	1	sseli 3224	. . 3 ⊢ (𝐴 ∈ P → 𝐴 ∈ (𝒫 Q × 𝒫 Q))
3		1st2nd2 6347	. . 3 ⊢ (𝐴 ∈ (𝒫 Q × 𝒫 Q) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
4	2, 3	syl 14	. 2 ⊢ (𝐴 ∈ P → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
5		eleq1 2294	. . 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 1398   ∈ wcel 2202  𝒫 cpw 3656  ⟨cop 3676   × cxp 4729  ‘cfv 5333  1^st c1st 6310  2^nd c2nd 6311  Qcnq 7543  Pcnp 7554

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-un 4536

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-sbc 3033  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-mpt 4157  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-iota 5293  df-fun 5335  df-fv 5341  df-1st 6312  df-2nd 6313  df-inp 7729

This theorem is referenced by:  elnp1st2nd  7739  0npr  7746  genpdf  7771  genipv  7772  genpelvl  7775  genpelvu  7776  genpml  7780  genpmu  7781  genprndl  7784  genprndu  7785  genpdisj  7786  genpassl  7787  genpassu  7788  addnqprl  7792  addnqpru  7793  addlocprlemeqgt  7795  addlocprlemgt  7797  addlocprlem  7798  addlocpr  7799  nqprl  7814  nqpru  7815  addnqprlemfl  7822  addnqprlemfu  7823  mulnqprl  7831  mulnqpru  7832  mullocprlem  7833  mullocpr  7834  mulnqprlemfl  7838  mulnqprlemfu  7839  addcomprg  7841  mulcomprg  7843  distrlem1prl  7845  distrlem1pru  7846  distrlem4prl  7847  distrlem4pru  7848  ltprordil  7852  1idprl  7853  1idpru  7854  ltpopr  7858  ltsopr  7859  ltaddpr  7860  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemlol  7865  ltexprlemopu  7866  ltexprlemupu  7867  ltexprlemdisj  7869  ltexprlemloc  7870  ltexprlemfl  7872  ltexprlemrl  7873  ltexprlemfu  7874  ltexprlemru  7875  addcanprleml  7877  addcanprlemu  7878  prplnqu  7883  recexprlemm  7887  recexprlemdisj  7893  recexprlemloc  7894  recexprlem1ssl  7896  recexprlem1ssu  7897  recexprlemss1l  7898  recexprlemss1u  7899  aptiprleml  7902  aptiprlemu  7903  archpr  7906  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  archrecpr  7927  caucvgprlemladdrl  7941  caucvgprprlemml  7957  caucvgprprlemmu  7958  caucvgprprlemopl  7960  suplocexprlemml  7979  suplocexprlemrl  7980  suplocexprlemmu  7981  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemex  7985  suplocexprlemub  7986