Theorem prop 7789

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 7785	. . . 4 ⊢ P ⊆ (𝒫 Q × 𝒫 Q)
2	1	sseli 3233	. . 3 ⊢ (𝐴 ∈ P → 𝐴 ∈ (𝒫 Q × 𝒫 Q))
3		1st2nd2 6368	. . 3 ⊢ (𝐴 ∈ (𝒫 Q × 𝒫 Q) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
4	2, 3	syl 14	. 2 ⊢ (𝐴 ∈ P → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
5		eleq1 2295	. . 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 2203  𝒫 cpw 3668  ⟨cop 3691   × cxp 4746  ‘cfv 5351  1^st c1st 6331  2^nd c2nd 6332  Qcnq 7594  Pcnp 7605

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 2205  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-pr 4321  ax-un 4553

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2814  df-sbc 3042  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-br 4109  df-opab 4171  df-mpt 4172  df-id 4413  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-rn 4759  df-iota 5311  df-fun 5353  df-fv 5359  df-1st 6333  df-2nd 6334  df-inp 7780

This theorem is referenced by:  elnp1st2nd  7790  0npr  7797  genpdf  7822  genipv  7823  genpelvl  7826  genpelvu  7827  genpml  7831  genpmu  7832  genprndl  7835  genprndu  7836  genpdisj  7837  genpassl  7838  genpassu  7839  addnqprl  7843  addnqpru  7844  addlocprlemeqgt  7846  addlocprlemgt  7848  addlocprlem  7849  addlocpr  7850  nqprl  7865  nqpru  7866  addnqprlemfl  7873  addnqprlemfu  7874  mulnqprl  7882  mulnqpru  7883  mullocprlem  7884  mullocpr  7885  mulnqprlemfl  7889  mulnqprlemfu  7890  addcomprg  7892  mulcomprg  7894  distrlem1prl  7896  distrlem1pru  7897  distrlem4prl  7898  distrlem4pru  7899  ltprordil  7903  1idprl  7904  1idpru  7905  ltpopr  7909  ltsopr  7910  ltaddpr  7911  ltexprlemm  7914  ltexprlemopl  7915  ltexprlemlol  7916  ltexprlemopu  7917  ltexprlemupu  7918  ltexprlemdisj  7920  ltexprlemloc  7921  ltexprlemfl  7923  ltexprlemrl  7924  ltexprlemfu  7925  ltexprlemru  7926  addcanprleml  7928  addcanprlemu  7929  prplnqu  7934  recexprlemm  7938  recexprlemdisj  7944  recexprlemloc  7945  recexprlem1ssl  7947  recexprlem1ssu  7948  recexprlemss1l  7949  recexprlemss1u  7950  aptiprleml  7953  aptiprlemu  7954  archpr  7957  cauappcvgprlemladdru  7970  cauappcvgprlemladdrl  7971  archrecpr  7978  caucvgprlemladdrl  7992  caucvgprprlemml  8008  caucvgprprlemmu  8009  caucvgprprlemopl  8011  suplocexprlemml  8030  suplocexprlemrl  8031  suplocexprlemmu  8032  suplocexprlemdisj  8034  suplocexprlemloc  8035  suplocexprlemex  8036  suplocexprlemub  8037