Metamath Proof Explorer


Definition df-ipo

Description: For any family of sets, define the poset of that family ordered by inclusion. See ipobas , ipolerval , and ipole 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.)

Ref Expression
Assertion 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 ) = (/) } ) >. } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cipo
 |-  toInc
1 vf
 |-  f
2 cvv
 |-  _V
3 vx
 |-  x
4 vy
 |-  y
5 3 cv
 |-  x
6 4 cv
 |-  y
7 5 6 cpr
 |-  { x , y }
8 1 cv
 |-  f
9 7 8 wss
 |-  { x , y } C_ f
10 5 6 wss
 |-  x C_ y
11 9 10 wa
 |-  ( { x , y } C_ f /\ x C_ y )
12 11 3 4 copab
 |-  { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) }
13 vo
 |-  o
14 cbs
 |-  Base
15 cnx
 |-  ndx
16 15 14 cfv
 |-  ( Base ` ndx )
17 16 8 cop
 |-  <. ( Base ` ndx ) , f >.
18 cts
 |-  TopSet
19 15 18 cfv
 |-  ( TopSet ` ndx )
20 cordt
 |-  ordTop
21 13 cv
 |-  o
22 21 20 cfv
 |-  ( ordTop ` o )
23 19 22 cop
 |-  <. ( TopSet ` ndx ) , ( ordTop ` o ) >.
24 17 23 cpr
 |-  { <. ( Base ` ndx ) , f >. , <. ( TopSet ` ndx ) , ( ordTop ` o ) >. }
25 cple
 |-  le
26 15 25 cfv
 |-  ( le ` ndx )
27 26 21 cop
 |-  <. ( le ` ndx ) , o >.
28 coc
 |-  oc
29 15 28 cfv
 |-  ( oc ` ndx )
30 6 5 cin
 |-  ( y i^i x )
31 c0
 |-  (/)
32 30 31 wceq
 |-  ( y i^i x ) = (/)
33 32 4 8 crab
 |-  { y e. f | ( y i^i x ) = (/) }
34 33 cuni
 |-  U. { y e. f | ( y i^i x ) = (/) }
35 3 8 34 cmpt
 |-  ( x e. f |-> U. { y e. f | ( y i^i x ) = (/) } )
36 29 35 cop
 |-  <. ( oc ` ndx ) , ( x e. f |-> U. { y e. f | ( y i^i x ) = (/) } ) >.
37 27 36 cpr
 |-  { <. ( le ` ndx ) , o >. , <. ( oc ` ndx ) , ( x e. f |-> U. { y e. f | ( y i^i x ) = (/) } ) >. }
38 24 37 cun
 |-  ( { <. ( Base ` ndx ) , f >. , <. ( TopSet ` ndx ) , ( ordTop ` o ) >. } u. { <. ( le ` ndx ) , o >. , <. ( oc ` ndx ) , ( x e. f |-> U. { y e. f | ( y i^i x ) = (/) } ) >. } )
39 13 12 38 csb
 |-  [_ { <. 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 ) = (/) } ) >. } )
40 1 2 39 cmpt
 |-  ( 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 ) = (/) } ) >. } ) )
41 0 40 wceq
 |-  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 ) = (/) } ) >. } ) )