Definition df-ipo 17152

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

Step	Hyp	Ref	Expression
1		cipo 17151	. 2 class toInc
2		vf	. . 3 setvar f
3		cvv 3200	. . 3 class _V
4		vo	. . . 4 setvar o
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1482	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1482	. . . . . . . 8 class y
9	6, 8	cpr 4179	. . . . . . 7 class { x , y }
10	2	cv 1482	. . . . . . 7 class f
11	9, 10	wss 3574	. . . . . 6 wff { x , y } C_ f
12	6, 8	wss 3574	. . . . . 6 wff x C_ y
13	11, 12	wa 384	. . . . 5 wff ( { x , y } C_ f /\ x C_ y )
14	13, 5, 7	copab 4712	. . . 4 class { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) }
15		cnx 15854	. . . . . . . 8 class ndx
16		cbs 15857	. . . . . . . 8 class Base
17	15, 16	cfv 5888	. . . . . . 7 class ( Base ` ndx )
18	17, 10	cop 4183	. . . . . 6 class <. ( Base ` ndx ) , f >.
19		cts 15947	. . . . . . . 8 class TopSet
20	15, 19	cfv 5888	. . . . . . 7 class (TopSet ` ndx )
21	4	cv 1482	. . . . . . . 8 class o
22		cordt 16159	. . . . . . . 8 class ordTop
23	21, 22	cfv 5888	. . . . . . 7 class (ordTop ` o )
24	20, 23	cop 4183	. . . . . 6 class <. (TopSet ` ndx ) , (ordTop ` o ) >.
25	18, 24	cpr 4179	. . . . 5 class { <. ( Base ` ndx ) , f >. , <. (TopSet ` ndx ) , (ordTop ` o ) >. }
26		cple 15948	. . . . . . . 8 class le
27	15, 26	cfv 5888	. . . . . . 7 class ( le ` ndx )
28	27, 21	cop 4183	. . . . . 6 class <. ( le ` ndx ) , o >.
29		coc 15949	. . . . . . . 8 class oc
30	15, 29	cfv 5888	. . . . . . 7 class ( oc ` ndx )
31	8, 6	cin 3573	. . . . . . . . . . 11 class ( y i^i x )
32		c0 3915	. . . . . . . . . . 11 class (/)
33	31, 32	wceq 1483	. . . . . . . . . 10 wff ( y i^i x ) = (/)
34	33, 7, 10	crab 2916	. . . . . . . . 9 class { y e. f | ( y i^i x ) = (/) }
35	34	cuni 4436	. . . . . . . 8 class U. { y e. f | ( y i^i x ) = (/) }
36	5, 10, 35	cmpt 4729	. . . . . . 7 class ( x e. f |-> U. { y e. f | ( y i^i x ) = (/) } )
37	30, 36	cop 4183	. . . . . 6 class <. ( oc ` ndx ) , ( x e. f |-> U. { y e. f | ( y i^i x ) = (/) } ) >.
38	28, 37	cpr 4179	. . . . 5 class { <. ( le ` ndx ) , o >. , <. ( oc ` ndx ) , ( x e. f |-> U. { y e. f | ( y i^i x ) = (/) } ) >. }
39	25, 38	cun 3572	. . . 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 ) = (/) } ) >. } )
40	4, 14, 39	csb 3533	. . 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 ) = (/) } ) >. } )
41	2, 3, 40	cmpt 4729	. 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 ) = (/) } ) >. } ) )
42	1, 41	wceq 1483	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 ) = (/) } ) >. } ) )

This definition is referenced by:  ipoval  17154