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	$$⊢\mathrm{toInc}=\left(f\in \mathrm{V}⟼⦋\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\right\}/o⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},f⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(o\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},o⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in f⟼\bigcup \left\{y\in f|y\cap x=\varnothing \right\}\right)⟩\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cipo	$$class\mathrm{toInc}$$
1		vf	$$setvarf$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		vy	$$setvary$$
5	3	cv	$$setvarx$$
6	4	cv	$$setvary$$
7	5 6	cpr	$$class\left\{x,y\right\}$$
8	1	cv	$$setvarf$$
9	7 8	wss	$$wff\left\{x,y\right\}\subseteq f$$
10	5 6	wss	$$wffx\subseteq y$$
11	9 10	wa	$$wff\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)$$
12	11 3 4	copab	$$class\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\right\}$$
13		vo	$$setvaro$$
14		cbs	$$class\mathrm{Base}$$
15		cnx	$$class\mathrm{ndx}$$
16	15 14	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
17	16 8	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},f⟩$$
18		cts	$$class\mathrm{TopSet}$$
19	15 18	cfv	$$class\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
20		cordt	$$class\mathrm{ordTop}$$
21	13	cv	$$setvaro$$
22	21 20	cfv	$$class\mathrm{ordTop}\left(o\right)$$
23	19 22	cop	$$class⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(o\right)⟩$$
24	17 23	cpr	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},f⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(o\right)⟩\right\}$$
25		cple	$$class\mathrm{le}$$
26	15 25	cfv	$$class{\le }_{\mathrm{ndx}}$$
27	26 21	cop	$$class⟨{\le }_{\mathrm{ndx}},o⟩$$
28		coc	$$class\mathrm{oc}$$
29	15 28	cfv	$$class\mathrm{oc}\left(\mathrm{ndx}\right)$$
30	6 5	cin	$$class\left(y\cap x\right)$$
31		c0	$$class\varnothing$$
32	30 31	wceq	$$wffy\cap x=\varnothing$$
33	32 4 8	crab	$$class\left\{y\in f|y\cap x=\varnothing \right\}$$
34	33	cuni	$$class\bigcup \left\{y\in f|y\cap x=\varnothing \right\}$$
35	3 8 34	cmpt	$$class\left(x\in f⟼\bigcup \left\{y\in f|y\cap x=\varnothing \right\}\right)$$
36	29 35	cop	$$class⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in f⟼\bigcup \left\{y\in f|y\cap x=\varnothing \right\}\right)⟩$$
37	27 36	cpr	$$class\left\{⟨{\le }_{\mathrm{ndx}},o⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in f⟼\bigcup \left\{y\in f|y\cap x=\varnothing \right\}\right)⟩\right\}$$
38	24 37	cun	$$class\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},f⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(o\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},o⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in f⟼\bigcup \left\{y\in f|y\cap x=\varnothing \right\}\right)⟩\right\}\right)$$
39	13 12 38	csb	$$class⦋\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\right\}/o⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},f⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(o\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},o⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in f⟼\bigcup \left\{y\in f|y\cap x=\varnothing \right\}\right)⟩\right\}\right)$$
40	1 2 39	cmpt	$$class\left(f\in \mathrm{V}⟼⦋\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\right\}/o⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},f⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(o\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},o⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in f⟼\bigcup \left\{y\in f|y\cap x=\varnothing \right\}\right)⟩\right\}\right)\right)$$
41	0 40	wceq	$$wff\mathrm{toInc}=\left(f\in \mathrm{V}⟼⦋\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\right\}/o⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},f⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(o\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},o⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in f⟼\bigcup \left\{y\in f|y\cap x=\varnothing \right\}\right)⟩\right\}\right)\right)$$