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