Theorem ltrelpr 7337

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 7302	. 2 |- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
2		opabssxp 4621	. 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 3134	1 |- <P C_ ( P. X. P. )

Syntax hints:   /\ wa 103   e. wcel 1481   E.wrex 2418   C_ wss 3076   {copab 3996   X. cxp 4545   ` cfv 5131   1stc1st 6044   2ndc2nd 6045   Q.cnq 7112   P.cnp 7123   <P cltp 7127

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-in 3082  df-ss 3089  df-opab 3998  df-xp 4553  df-iltp 7302

This theorem is referenced by:  ltprordil  7421  ltexprlemm  7432  ltexprlemopl  7433  ltexprlemlol  7434  ltexprlemopu  7435  ltexprlemupu  7436  ltexprlemdisj  7438  ltexprlemloc  7439  ltexprlemfl  7441  ltexprlemrl  7442  ltexprlemfu  7443  ltexprlemru  7444  ltexpri  7445  lteupri  7449  ltaprlem  7450  prplnqu  7452  caucvgprprlemk  7515  caucvgprprlemnkltj  7521  caucvgprprlemnkeqj  7522  caucvgprprlemnjltk  7523  caucvgprprlemnbj  7525  caucvgprprlemml  7526  caucvgprprlemlol  7530  caucvgprprlemupu  7532  suplocexprlemss  7547  suplocexprlemlub  7556  gt0srpr  7580  lttrsr  7594  ltposr  7595  archsr  7614