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

Theorem nqprlu 6645
 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 3768 . . . . 5 (𝑙 = 𝑎 → (𝐴 <Q 𝑙𝐴 <Q 𝑎))
21cbvabv 2161 . . . 4 {𝑙𝐴 <Q 𝑙} = {𝑎𝐴 <Q 𝑎}
3 breq2 3768 . . . . 5 (𝑢 = 𝑎 → (𝐴 <Q 𝑢𝐴 <Q 𝑎))
43cbvabv 2161 . . . 4 {𝑢𝐴 <Q 𝑢} = {𝑎𝐴 <Q 𝑎}
52, 4eqtr4i 2063 . . 3 {𝑙𝐴 <Q 𝑙} = {𝑢𝐴 <Q 𝑢}
65opeq2i 3553 . 2 ⟨{𝑙𝑙 <Q 𝐴}, {𝑙𝐴 <Q 𝑙}⟩ = ⟨{𝑙𝑙 <Q 𝐴}, {𝑢𝐴 <Q 𝑢}⟩
7 nqprxx 6644 . 2 (𝐴Q → ⟨{𝑙𝑙 <Q 𝐴}, {𝑙𝐴 <Q 𝑙}⟩ ∈ P)
86, 7syl5eqelr 2125 1 (𝐴Q → ⟨{𝑙𝑙 <Q 𝐴}, {𝑢𝐴 <Q 𝑢}⟩ ∈ P)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 1393  {cab 2026  ⟨cop 3378   class class class wbr 3764  Qcnq 6378
 Copyright terms: Public domain W3C validator