MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ipo Structured version   Unicode version

Definition df-ipo 15981
Description: For any family of sets, define the poset of that family ordered by inclusion. See ipobas 15984, ipolerval 15985, and ipole 15987 for its contract.

EDITORIAL: I'm not thrilled with the name. Any suggestions? (Contributed by Stefan O'Rear, 30-Jan-2015.) (New usage is discouraged.)

Assertion
Ref Expression
df-ipo  |- toInc  =  ( f  e.  _V  |->  [_ { <. x ,  y
>.  |  ( {
x ,  y } 
C_  f  /\  x  C_  y ) }  / 
o ]_ ( { <. (
Base `  ndx ) ,  f >. ,  <. (TopSet ` 
ndx ) ,  (ordTop `  o ) >. }  u.  {
<. ( le `  ndx ) ,  o >. , 
<. ( oc `  ndx ) ,  ( x  e.  f  |->  U. {
y  e.  f  |  ( y  i^i  x
)  =  (/) } )
>. } ) )
Distinct variable group:    f, o, x, y

Detailed syntax breakdown of Definition df-ipo
StepHypRef Expression
1 cipo 15980 . 2  class toInc
2 vf . . 3  setvar  f
3 cvv 3106 . . 3  class  _V
4 vo . . . 4  setvar  o
5 vx . . . . . . . . 9  setvar  x
65cv 1397 . . . . . . . 8  class  x
7 vy . . . . . . . . 9  setvar  y
87cv 1397 . . . . . . . 8  class  y
96, 8cpr 4018 . . . . . . 7  class  { x ,  y }
102cv 1397 . . . . . . 7  class  f
119, 10wss 3461 . . . . . 6  wff  { x ,  y }  C_  f
126, 8wss 3461 . . . . . 6  wff  x  C_  y
1311, 12wa 367 . . . . 5  wff  ( { x ,  y } 
C_  f  /\  x  C_  y )
1413, 5, 7copab 4496 . . . 4  class  { <. x ,  y >.  |  ( { x ,  y }  C_  f  /\  x  C_  y ) }
15 cnx 14713 . . . . . . . 8  class  ndx
16 cbs 14716 . . . . . . . 8  class  Base
1715, 16cfv 5570 . . . . . . 7  class  ( Base `  ndx )
1817, 10cop 4022 . . . . . 6  class  <. ( Base `  ndx ) ,  f >.
19 cts 14790 . . . . . . . 8  class TopSet
2015, 19cfv 5570 . . . . . . 7  class  (TopSet `  ndx )
214cv 1397 . . . . . . . 8  class  o
22 cordt 14988 . . . . . . . 8  class ordTop
2321, 22cfv 5570 . . . . . . 7  class  (ordTop `  o )
2420, 23cop 4022 . . . . . 6  class  <. (TopSet ` 
ndx ) ,  (ordTop `  o ) >.
2518, 24cpr 4018 . . . . 5  class  { <. (
Base `  ndx ) ,  f >. ,  <. (TopSet ` 
ndx ) ,  (ordTop `  o ) >. }
26 cple 14791 . . . . . . . 8  class  le
2715, 26cfv 5570 . . . . . . 7  class  ( le
`  ndx )
2827, 21cop 4022 . . . . . 6  class  <. ( le `  ndx ) ,  o >.
29 coc 14792 . . . . . . . 8  class  oc
3015, 29cfv 5570 . . . . . . 7  class  ( oc
`  ndx )
318, 6cin 3460 . . . . . . . . . . 11  class  ( y  i^i  x )
32 c0 3783 . . . . . . . . . . 11  class  (/)
3331, 32wceq 1398 . . . . . . . . . 10  wff  ( y  i^i  x )  =  (/)
3433, 7, 10crab 2808 . . . . . . . . 9  class  { y  e.  f  |  ( y  i^i  x )  =  (/) }
3534cuni 4235 . . . . . . . 8  class  U. {
y  e.  f  |  ( y  i^i  x
)  =  (/) }
365, 10, 35cmpt 4497 . . . . . . 7  class  ( x  e.  f  |->  U. {
y  e.  f  |  ( y  i^i  x
)  =  (/) } )
3730, 36cop 4022 . . . . . 6  class  <. ( oc `  ndx ) ,  ( x  e.  f 
|->  U. { y  e.  f  |  ( y  i^i  x )  =  (/) } ) >.
3828, 37cpr 4018 . . . . 5  class  { <. ( le `  ndx ) ,  o >. ,  <. ( oc `  ndx ) ,  ( x  e.  f  |->  U. { y  e.  f  |  ( y  i^i  x )  =  (/) } ) >. }
3925, 38cun 3459 . . . 4  class  ( {
<. ( Base `  ndx ) ,  f >. , 
<. (TopSet `  ndx ) ,  (ordTop `  o ) >. }  u.  { <. ( le `  ndx ) ,  o >. ,  <. ( oc `  ndx ) ,  ( x  e.  f  |->  U. { y  e.  f  |  ( y  i^i  x )  =  (/) } ) >. } )
404, 14, 39csb 3420 . . 3  class  [_ { <. x ,  y >.  |  ( { x ,  y }  C_  f  /\  x  C_  y
) }  /  o ]_ ( { <. ( Base `  ndx ) ,  f >. ,  <. (TopSet ` 
ndx ) ,  (ordTop `  o ) >. }  u.  {
<. ( le `  ndx ) ,  o >. , 
<. ( oc `  ndx ) ,  ( x  e.  f  |->  U. {
y  e.  f  |  ( y  i^i  x
)  =  (/) } )
>. } )
412, 3, 40cmpt 4497 . 2  class  ( f  e.  _V  |->  [_ { <. x ,  y >.  |  ( { x ,  y }  C_  f  /\  x  C_  y
) }  /  o ]_ ( { <. ( Base `  ndx ) ,  f >. ,  <. (TopSet ` 
ndx ) ,  (ordTop `  o ) >. }  u.  {
<. ( le `  ndx ) ,  o >. , 
<. ( oc `  ndx ) ,  ( x  e.  f  |->  U. {
y  e.  f  |  ( y  i^i  x
)  =  (/) } )
>. } ) )
421, 41wceq 1398 1  wff toInc  =  ( f  e.  _V  |->  [_ { <. x ,  y
>.  |  ( {
x ,  y } 
C_  f  /\  x  C_  y ) }  / 
o ]_ ( { <. (
Base `  ndx ) ,  f >. ,  <. (TopSet ` 
ndx ) ,  (ordTop `  o ) >. }  u.  {
<. ( le `  ndx ) ,  o >. , 
<. ( oc `  ndx ) ,  ( x  e.  f  |->  U. {
y  e.  f  |  ( y  i^i  x
)  =  (/) } )
>. } ) )
Colors of variables: wff setvar class
This definition is referenced by:  ipoval  15983
  Copyright terms: Public domain W3C validator