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 3991 | . . . . 5 ⊢ (𝑙 = 𝑎 → (𝐴 <Q 𝑙 ↔ 𝐴 <Q 𝑎)) | |
2 | 1 | cbvabv 2295 | . . . 4 ⊢ {𝑙 ∣ 𝐴 <Q 𝑙} = {𝑎 ∣ 𝐴 <Q 𝑎} |
3 | breq2 3991 | . . . . 5 ⊢ (𝑢 = 𝑎 → (𝐴 <Q 𝑢 ↔ 𝐴 <Q 𝑎)) | |
4 | 3 | cbvabv 2295 | . . . 4 ⊢ {𝑢 ∣ 𝐴 <Q 𝑢} = {𝑎 ∣ 𝐴 <Q 𝑎} |
5 | 2, 4 | eqtr4i 2194 | . . 3 ⊢ {𝑙 ∣ 𝐴 <Q 𝑙} = {𝑢 ∣ 𝐴 <Q 𝑢} |
6 | 5 | opeq2i 3767 | . 2 ⊢ 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑙 ∣ 𝐴 <Q 𝑙}〉 = 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 |
7 | nqprxx 7495 | . 2 ⊢ (𝐴 ∈ Q → 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑙 ∣ 𝐴 <Q 𝑙}〉 ∈ P) | |
8 | 6, 7 | eqeltrrid 2258 | 1 ⊢ (𝐴 ∈ Q → 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ∈ P) |
Copyright terms: Public domain | W3C validator |