Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ltrelnq | GIF version |
Description: Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.) |
Ref | Expression |
---|---|
ltrelnq | ⊢ <Q ⊆ (Q × Q) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ltnqqs 7315 | . 2 ⊢ <Q = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ~Q ∧ 𝑦 = [〈𝑣, 𝑢〉] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))} | |
2 | opabssxp 4685 | . 2 ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ~Q ∧ 𝑦 = [〈𝑣, 𝑢〉] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))} ⊆ (Q × Q) | |
3 | 1, 2 | eqsstri 3179 | 1 ⊢ <Q ⊆ (Q × Q) |
Copyright terms: Public domain | W3C validator |