Theorem ltrelpr 7620

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

Assertion

Ref	Expression
ltrelpr	|- <P C_ ( P. X. P. )

Proof of Theorem ltrelpr

Dummy variables x q y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iltp 7585	. 2 |- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
2		opabssxp 4750	. 2 |- { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) } C_ ( P. X. P. )
3	1, 2	eqsstri 3225	1 |- <P C_ ( P. X. P. )

Syntax hints:   /\ wa 104   e. wcel 2176   E.wrex 2485   C_ wss 3166   {copab 4105   X. cxp 4674   ` cfv 5272   1stc1st 6226   2ndc2nd 6227   Q.cnq 7395   P.cnp 7406   <P cltp 7410

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 4107  df-xp 4682  df-iltp 7585

This theorem is referenced by:  ltprordil  7704  ltexprlemm  7715  ltexprlemopl  7716  ltexprlemlol  7717  ltexprlemopu  7718  ltexprlemupu  7719  ltexprlemdisj  7721  ltexprlemloc  7722  ltexprlemfl  7724  ltexprlemrl  7725  ltexprlemfu  7726  ltexprlemru  7727  ltexpri  7728  lteupri  7732  ltaprlem  7733  prplnqu  7735  caucvgprprlemk  7798  caucvgprprlemnkltj  7804  caucvgprprlemnkeqj  7805  caucvgprprlemnjltk  7806  caucvgprprlemnbj  7808  caucvgprprlemml  7809  caucvgprprlemlol  7813  caucvgprprlemupu  7815  suplocexprlemss  7830  suplocexprlemlub  7839  gt0srpr  7863  lttrsr  7877  ltposr  7878  archsr  7897