Theorem ltrelpr 7467

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 7432	. 2 ⊢ <P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧ ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦)))}
2		opabssxp 4685	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧ ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦)))} ⊆ (P × P)
3	1, 2	eqsstri 3179	1 ⊢ <P ⊆ (P × P)

Syntax hints:   ∧ wa 103   ∈ wcel 2141  ∃wrex 2449   ⊆ wss 3121  {copab 4049   × cxp 4609  ‘cfv 5198  1^st c1st 6117  2^nd c2nd 6118  Qcnq 7242  Pcnp 7253  <_P cltp 7257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-in 3127  df-ss 3134  df-opab 4051  df-xp 4617  df-iltp 7432

This theorem is referenced by:  ltprordil  7551  ltexprlemm  7562  ltexprlemopl  7563  ltexprlemlol  7564  ltexprlemopu  7565  ltexprlemupu  7566  ltexprlemdisj  7568  ltexprlemloc  7569  ltexprlemfl  7571  ltexprlemrl  7572  ltexprlemfu  7573  ltexprlemru  7574  ltexpri  7575  lteupri  7579  ltaprlem  7580  prplnqu  7582  caucvgprprlemk  7645  caucvgprprlemnkltj  7651  caucvgprprlemnkeqj  7652  caucvgprprlemnjltk  7653  caucvgprprlemnbj  7655  caucvgprprlemml  7656  caucvgprprlemlol  7660  caucvgprprlemupu  7662  suplocexprlemss  7677  suplocexprlemlub  7686  gt0srpr  7710  lttrsr  7724  ltposr  7725  archsr  7744