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

Theorem ltrelnq 6463
 Description: Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.)
Assertion
Ref Expression
ltrelnq <Q ⊆ (Q × Q)

Proof of Theorem ltrelnq
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ltnqqs 6451 . 2 <Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}
2 opabssxp 4414 . 2 {⟨𝑥, 𝑦⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))} ⊆ (Q × Q)
31, 2eqsstri 2975 1 <Q ⊆ (Q × Q)
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   = wceq 1243  ∃wex 1381   ∈ wcel 1393   ⊆ wss 2917  ⟨cop 3378   class class class wbr 3764  {copab 3817   × cxp 4343  (class class class)co 5512  [cec 6104   ·N cmi 6372
 Copyright terms: Public domain W3C validator