Theorem ltrelpr 7437

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

Syntax hints:   ∧ wa 103   ∈ wcel 2135  ∃wrex 2443   ⊆ wss 3111  {copab 4036   × cxp 4596  ‘cfv 5182  1^st c1st 6098  2^nd c2nd 6099  Qcnq 7212  Pcnp 7223  <_P cltp 7227

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 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-in 3117  df-ss 3124  df-opab 4038  df-xp 4604  df-iltp 7402

This theorem is referenced by:  ltprordil  7521  ltexprlemm  7532  ltexprlemopl  7533  ltexprlemlol  7534  ltexprlemopu  7535  ltexprlemupu  7536  ltexprlemdisj  7538  ltexprlemloc  7539  ltexprlemfl  7541  ltexprlemrl  7542  ltexprlemfu  7543  ltexprlemru  7544  ltexpri  7545  lteupri  7549  ltaprlem  7550  prplnqu  7552  caucvgprprlemk  7615  caucvgprprlemnkltj  7621  caucvgprprlemnkeqj  7622  caucvgprprlemnjltk  7623  caucvgprprlemnbj  7625  caucvgprprlemml  7626  caucvgprprlemlol  7630  caucvgprprlemupu  7632  suplocexprlemss  7647  suplocexprlemlub  7656  gt0srpr  7680  lttrsr  7694  ltposr  7695  archsr  7714