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