Theorem ltrelpr 7692

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

Syntax hints:   /\ wa 104   e. wcel 2200   E.wrex 2509   C_ wss 3197   {copab 4144   X. cxp 4717   ` cfv 5318   1stc1st 6284   2ndc2nd 6285   Q.cnq 7467   P.cnp 7478   <P cltp 7482

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-in 3203  df-ss 3210  df-opab 4146  df-xp 4725  df-iltp 7657

This theorem is referenced by:  ltprordil  7776  ltexprlemm  7787  ltexprlemopl  7788  ltexprlemlol  7789  ltexprlemopu  7790  ltexprlemupu  7791  ltexprlemdisj  7793  ltexprlemloc  7794  ltexprlemfl  7796  ltexprlemrl  7797  ltexprlemfu  7798  ltexprlemru  7799  ltexpri  7800  lteupri  7804  ltaprlem  7805  prplnqu  7807  caucvgprprlemk  7870  caucvgprprlemnkltj  7876  caucvgprprlemnkeqj  7877  caucvgprprlemnjltk  7878  caucvgprprlemnbj  7880  caucvgprprlemml  7881  caucvgprprlemlol  7885  caucvgprprlemupu  7887  suplocexprlemss  7902  suplocexprlemlub  7911  gt0srpr  7935  lttrsr  7949  ltposr  7950  archsr  7969