Theorem ltrelpr 7618

Description: Positive real 'less than' is a relation on positive reals. (Contributed by NM, 14-Feb-1996.)

Assertion

Ref	Expression
ltrelpr	⊢ <P ⊆ (P × P)

Proof of Theorem ltrelpr

Dummy variables 𝑥 𝑞 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iltp 7583	. 2 ⊢ <P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧ ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦)))}
2		opabssxp 4749	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧ ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦)))} ⊆ (P × P)
3	1, 2	eqsstri 3225	1 ⊢ <P ⊆ (P × P)

Syntax hints:   ∧ wa 104   ∈ wcel 2176  ∃wrex 2485   ⊆ wss 3166  {copab 4104   × cxp 4673  ‘cfv 5271  1^st c1st 6224  2^nd c2nd 6225  Qcnq 7393  Pcnp 7404  <_P cltp 7408

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-in 3172  df-ss 3179  df-opab 4106  df-xp 4681  df-iltp 7583

This theorem is referenced by:  ltprordil  7702  ltexprlemm  7713  ltexprlemopl  7714  ltexprlemlol  7715  ltexprlemopu  7716  ltexprlemupu  7717  ltexprlemdisj  7719  ltexprlemloc  7720  ltexprlemfl  7722  ltexprlemrl  7723  ltexprlemfu  7724  ltexprlemru  7725  ltexpri  7726  lteupri  7730  ltaprlem  7731  prplnqu  7733  caucvgprprlemk  7796  caucvgprprlemnkltj  7802  caucvgprprlemnkeqj  7803  caucvgprprlemnjltk  7804  caucvgprprlemnbj  7806  caucvgprprlemml  7807  caucvgprprlemlol  7811  caucvgprprlemupu  7813  suplocexprlemss  7828  suplocexprlemlub  7837  gt0srpr  7861  lttrsr  7875  ltposr  7876  archsr  7895