ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nqprlu GIF version

Theorem nqprlu 7027
Description: The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.)
Assertion
Ref Expression
nqprlu (𝐴Q → ⟨{𝑙𝑙 <Q 𝐴}, {𝑢𝐴 <Q 𝑢}⟩ ∈ P)
Distinct variable groups:   𝐴,𝑙   𝑢,𝐴

Proof of Theorem nqprlu
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 breq2 3818 . . . . 5 (𝑙 = 𝑎 → (𝐴 <Q 𝑙𝐴 <Q 𝑎))
21cbvabv 2208 . . . 4 {𝑙𝐴 <Q 𝑙} = {𝑎𝐴 <Q 𝑎}
3 breq2 3818 . . . . 5 (𝑢 = 𝑎 → (𝐴 <Q 𝑢𝐴 <Q 𝑎))
43cbvabv 2208 . . . 4 {𝑢𝐴 <Q 𝑢} = {𝑎𝐴 <Q 𝑎}
52, 4eqtr4i 2108 . . 3 {𝑙𝐴 <Q 𝑙} = {𝑢𝐴 <Q 𝑢}
65opeq2i 3603 . 2 ⟨{𝑙𝑙 <Q 𝐴}, {𝑙𝐴 <Q 𝑙}⟩ = ⟨{𝑙𝑙 <Q 𝐴}, {𝑢𝐴 <Q 𝑢}⟩
7 nqprxx 7026 . 2 (𝐴Q → ⟨{𝑙𝑙 <Q 𝐴}, {𝑙𝐴 <Q 𝑙}⟩ ∈ P)
86, 7syl5eqelr 2172 1 (𝐴Q → ⟨{𝑙𝑙 <Q 𝐴}, {𝑢𝐴 <Q 𝑢}⟩ ∈ P)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1436  {cab 2071  cop 3428   class class class wbr 3814  Qcnq 6760   <Q cltq 6765  Pcnp 6771
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-in1 577  ax-in2 578  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-coll 3922  ax-sep 3925  ax-nul 3933  ax-pow 3977  ax-pr 4003  ax-un 4227  ax-setind 4319  ax-iinf 4369
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  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-ne 2252  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2616  df-sbc 2829  df-csb 2922  df-dif 2988  df-un 2990  df-in 2992  df-ss 2999  df-nul 3273  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-int 3666  df-iun 3709  df-br 3815  df-opab 3869  df-mpt 3870  df-tr 3905  df-eprel 4083  df-id 4087  df-po 4090  df-iso 4091  df-iord 4160  df-on 4162  df-suc 4165  df-iom 4372  df-xp 4410  df-rel 4411  df-cnv 4412  df-co 4413  df-dm 4414  df-rn 4415  df-res 4416  df-ima 4417  df-iota 4937  df-fun 4974  df-fn 4975  df-f 4976  df-f1 4977  df-fo 4978  df-f1o 4979  df-fv 4980  df-ov 5597  df-oprab 5598  df-mpt2 5599  df-1st 5849  df-2nd 5850  df-recs 6005  df-irdg 6070  df-1o 6116  df-oadd 6120  df-omul 6121  df-er 6225  df-ec 6227  df-qs 6231  df-ni 6784  df-pli 6785  df-mi 6786  df-lti 6787  df-plpq 6824  df-mpq 6825  df-enq 6827  df-nqqs 6828  df-plqqs 6829  df-mqqs 6830  df-1nqqs 6831  df-rq 6832  df-ltnqqs 6833  df-inp 6946
This theorem is referenced by:  recnnpr  7028  nqprl  7031  nqpru  7032  nnprlu  7033  1pr  7034  addnqprlemrl  7037  addnqprlemru  7038  addnqprlemfl  7039  addnqprlemfu  7040  addnqpr  7041  mulnqprlemrl  7053  mulnqprlemru  7054  mulnqprlemfl  7055  mulnqprlemfu  7056  mulnqpr  7057  ltnqpr  7073  ltnqpri  7074  prplnqu  7100  caucvgprlemcanl  7124  cauappcvgprlemladdfu  7134  cauappcvgprlemladdfl  7135  cauappcvgprlemladdru  7136  cauappcvgprlemladdrl  7137  cauappcvgprlemladd  7138  cauappcvgprlem1  7139  cauappcvgprlem2  7140  caucvgprlemladdfu  7157  caucvgprlemladdrl  7158  caucvgprlem1  7159  caucvgprlem2  7160  caucvgprprlemnkltj  7169  caucvgprprlemnkeqj  7170  caucvgprprlemmu  7175  caucvgprprlemopu  7179  caucvgprprlemloc  7183  caucvgprprlemexbt  7186  caucvgprprlem1  7189  caucvgprprlem2  7190  ltrennb  7312
  Copyright terms: Public domain W3C validator