![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nqprlu | GIF version |
Description: The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.) |
Ref | Expression |
---|---|
nqprlu | ⊢ (𝐴 ∈ Q → ⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ ∈ P) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq2 4007 | . . . . 5 ⊢ (𝑙 = 𝑎 → (𝐴 <Q 𝑙 ↔ 𝐴 <Q 𝑎)) | |
2 | 1 | cbvabv 2302 | . . . 4 ⊢ {𝑙 ∣ 𝐴 <Q 𝑙} = {𝑎 ∣ 𝐴 <Q 𝑎} |
3 | breq2 4007 | . . . . 5 ⊢ (𝑢 = 𝑎 → (𝐴 <Q 𝑢 ↔ 𝐴 <Q 𝑎)) | |
4 | 3 | cbvabv 2302 | . . . 4 ⊢ {𝑢 ∣ 𝐴 <Q 𝑢} = {𝑎 ∣ 𝐴 <Q 𝑎} |
5 | 2, 4 | eqtr4i 2201 | . . 3 ⊢ {𝑙 ∣ 𝐴 <Q 𝑙} = {𝑢 ∣ 𝐴 <Q 𝑢} |
6 | 5 | opeq2i 3782 | . 2 ⊢ ⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑙 ∣ 𝐴 <Q 𝑙}⟩ = ⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ |
7 | nqprxx 7544 | . 2 ⊢ (𝐴 ∈ Q → ⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑙 ∣ 𝐴 <Q 𝑙}⟩ ∈ P) | |
8 | 6, 7 | eqeltrrid 2265 | 1 ⊢ (𝐴 ∈ Q → ⟨{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}⟩ ∈ P) |
Copyright terms: Public domain | W3C validator |