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

Definition df-ipo 14255
Description: For any family of sets, define the poset of that family ordered by inclusion. See ipobas 14258, ipolerval 14259, and ipole 14261 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 14254 . 2  class toInc
2 vf . . 3  set  f
3 cvv 2788 . . 3  class  _V
4 vo . . . 4  set  o
5 vx . . . . . . . . 9  set  x
65cv 1622 . . . . . . . 8  class  x
7 vy . . . . . . . . 9  set  y
87cv 1622 . . . . . . . 8  class  y
96, 8cpr 3641 . . . . . . 7  class  { x ,  y }
102cv 1622 . . . . . . 7  class  f
119, 10wss 3152 . . . . . 6  wff  { x ,  y }  C_  f
126, 8wss 3152 . . . . . 6  wff  x  C_  y
1311, 12wa 358 . . . . 5  wff  ( { x ,  y } 
C_  f  /\  x  C_  y )
1413, 5, 7copab 4076 . . . 4  class  { <. x ,  y >.  |  ( { x ,  y }  C_  f  /\  x  C_  y ) }
15 cnx 13145 . . . . . . . 8  class  ndx
16 cbs 13148 . . . . . . . 8  class  Base
1715, 16cfv 5255 . . . . . . 7  class  ( Base `  ndx )
1817, 10cop 3643 . . . . . 6  class  <. ( Base `  ndx ) ,  f >.
19 cts 13214 . . . . . . . 8  class TopSet
2015, 19cfv 5255 . . . . . . 7  class  (TopSet `  ndx )
214cv 1622 . . . . . . . 8  class  o
22 cordt 13398 . . . . . . . 8  class ordTop
2321, 22cfv 5255 . . . . . . 7  class  (ordTop `  o )
2420, 23cop 3643 . . . . . 6  class  <. (TopSet ` 
ndx ) ,  (ordTop `  o ) >.
2518, 24cpr 3641 . . . . 5  class  { <. (
Base `  ndx ) ,  f >. ,  <. (TopSet ` 
ndx ) ,  (ordTop `  o ) >. }
26 cple 13215 . . . . . . . 8  class  le
2715, 26cfv 5255 . . . . . . 7  class  ( le
`  ndx )
2827, 21cop 3643 . . . . . 6  class  <. ( le `  ndx ) ,  o >.
29 coc 13216 . . . . . . . 8  class  oc
3015, 29cfv 5255 . . . . . . 7  class  ( oc
`  ndx )
318, 6cin 3151 . . . . . . . . . . 11  class  ( y  i^i  x )
32 c0 3455 . . . . . . . . . . 11  class  (/)
3331, 32wceq 1623 . . . . . . . . . 10  wff  ( y  i^i  x )  =  (/)
3433, 7, 10crab 2547 . . . . . . . . 9  class  { y  e.  f  |  ( y  i^i  x )  =  (/) }
3534cuni 3827 . . . . . . . 8  class  U. {
y  e.  f  |  ( y  i^i  x
)  =  (/) }
365, 10, 35cmpt 4077 . . . . . . 7  class  ( x  e.  f  |->  U. {
y  e.  f  |  ( y  i^i  x
)  =  (/) } )
3730, 36cop 3643 . . . . . 6  class  <. ( oc `  ndx ) ,  ( x  e.  f 
|->  U. { y  e.  f  |  ( y  i^i  x )  =  (/) } ) >.
3828, 37cpr 3641 . . . . 5  class  { <. ( le `  ndx ) ,  o >. ,  <. ( oc `  ndx ) ,  ( x  e.  f  |->  U. { y  e.  f  |  ( y  i^i  x )  =  (/) } ) >. }
3925, 38cun 3150 . . . 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 3081 . . 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 4077 . 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 1623 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 set class
This definition is referenced by:  ipoval  14257
  Copyright terms: Public domain W3C validator