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

Definition df-ipo 15334
Description: For any family of sets, define the poset of that family ordered by inclusion. See ipobas 15337, ipolerval 15338, and ipole 15340 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 15333 . 2  class toInc
2 vf . . 3  setvar  f
3 cvv 2984 . . 3  class  _V
4 vo . . . 4  setvar  o
5 vx . . . . . . . . 9  setvar  x
65cv 1368 . . . . . . . 8  class  x
7 vy . . . . . . . . 9  setvar  y
87cv 1368 . . . . . . . 8  class  y
96, 8cpr 3891 . . . . . . 7  class  { x ,  y }
102cv 1368 . . . . . . 7  class  f
119, 10wss 3340 . . . . . 6  wff  { x ,  y }  C_  f
126, 8wss 3340 . . . . . 6  wff  x  C_  y
1311, 12wa 369 . . . . 5  wff  ( { x ,  y } 
C_  f  /\  x  C_  y )
1413, 5, 7copab 4361 . . . 4  class  { <. x ,  y >.  |  ( { x ,  y }  C_  f  /\  x  C_  y ) }
15 cnx 14183 . . . . . . . 8  class  ndx
16 cbs 14186 . . . . . . . 8  class  Base
1715, 16cfv 5430 . . . . . . 7  class  ( Base `  ndx )
1817, 10cop 3895 . . . . . 6  class  <. ( Base `  ndx ) ,  f >.
19 cts 14256 . . . . . . . 8  class TopSet
2015, 19cfv 5430 . . . . . . 7  class  (TopSet `  ndx )
214cv 1368 . . . . . . . 8  class  o
22 cordt 14449 . . . . . . . 8  class ordTop
2321, 22cfv 5430 . . . . . . 7  class  (ordTop `  o )
2420, 23cop 3895 . . . . . 6  class  <. (TopSet ` 
ndx ) ,  (ordTop `  o ) >.
2518, 24cpr 3891 . . . . 5  class  { <. (
Base `  ndx ) ,  f >. ,  <. (TopSet ` 
ndx ) ,  (ordTop `  o ) >. }
26 cple 14257 . . . . . . . 8  class  le
2715, 26cfv 5430 . . . . . . 7  class  ( le
`  ndx )
2827, 21cop 3895 . . . . . 6  class  <. ( le `  ndx ) ,  o >.
29 coc 14258 . . . . . . . 8  class  oc
3015, 29cfv 5430 . . . . . . 7  class  ( oc
`  ndx )
318, 6cin 3339 . . . . . . . . . . 11  class  ( y  i^i  x )
32 c0 3649 . . . . . . . . . . 11  class  (/)
3331, 32wceq 1369 . . . . . . . . . 10  wff  ( y  i^i  x )  =  (/)
3433, 7, 10crab 2731 . . . . . . . . 9  class  { y  e.  f  |  ( y  i^i  x )  =  (/) }
3534cuni 4103 . . . . . . . 8  class  U. {
y  e.  f  |  ( y  i^i  x
)  =  (/) }
365, 10, 35cmpt 4362 . . . . . . 7  class  ( x  e.  f  |->  U. {
y  e.  f  |  ( y  i^i  x
)  =  (/) } )
3730, 36cop 3895 . . . . . 6  class  <. ( oc `  ndx ) ,  ( x  e.  f 
|->  U. { y  e.  f  |  ( y  i^i  x )  =  (/) } ) >.
3828, 37cpr 3891 . . . . 5  class  { <. ( le `  ndx ) ,  o >. ,  <. ( oc `  ndx ) ,  ( x  e.  f  |->  U. { y  e.  f  |  ( y  i^i  x )  =  (/) } ) >. }
3925, 38cun 3338 . . . 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 3300 . . 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 4362 . 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 1369 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  15336
  Copyright terms: Public domain W3C validator