Theorem ipoval

Description: Value of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Hypotheses	ipoval.i	$$⊢I=\mathrm{toInc}\left(F\right)$$
	ipoval.l	$$⊢\underset{\dot{}}{\le }=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}$$
Assertion	ipoval	$$⊢F\in V\to I=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ipoval.i	$$⊢I=\mathrm{toInc}\left(F\right)$$
2		ipoval.l	$$⊢\underset{\dot{}}{\le }=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}$$
3		elex	$$⊢F\in V\to F\in \mathrm{V}$$
4		vex	$$⊢f\in \mathrm{V}$$
5	4 4	xpex	$$⊢f\times f\in \mathrm{V}$$
6		vex	$$⊢x\in \mathrm{V}$$
7		vex	$$⊢y\in \mathrm{V}$$
8	6 7	prss	$$⊢\left(x\in f\wedge y\in f\right)\leftrightarrow \left\{x,y\right\}\subseteq f$$
9	8	biranri	$$⊢\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\to \left(x\in f\wedge y\in f\right)$$
10	9	ssopab2i	$$⊢\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\right\}\subseteq \left\{⟨x,y⟩|\left(x\in f\wedge y\in f\right)\right\}$$
11		df-xp	$$⊢f\times f=\left\{⟨x,y⟩|\left(x\in f\wedge y\in f\right)\right\}$$
12	10 11	sseqtrri	$$⊢\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\right\}\subseteq f\times f$$
13	5 12	ssexi	$$⊢\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\right\}\in \mathrm{V}$$
14	13	a1i	$$⊢f=F\to \left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\right\}\in \mathrm{V}$$
15		sseq2	$$⊢f=F\to \left(\left\{x,y\right\}\subseteq f\leftrightarrow \left\{x,y\right\}\subseteq F\right)$$
16	15	anbi1d	$$⊢f=F\to \left(\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\leftrightarrow \left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right)$$
17	16	opabbidv	$$⊢f=F\to \left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\right\}=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}$$
18	17 2	eqtr4di	$$⊢f=F\to \left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\right\}=\underset{\dot{}}{\le }$$
19		simpl	$$⊢\left(f=F\wedge o=\underset{\dot{}}{\le }\right)\to f=F$$
20	19	opeq2d	$$⊢\left(f=F\wedge o=\underset{\dot{}}{\le }\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},f⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩$$
21		simpr	$$⊢\left(f=F\wedge o=\underset{\dot{}}{\le }\right)\to o=\underset{\dot{}}{\le }$$
22	21	fveq2d	$$⊢\left(f=F\wedge o=\underset{\dot{}}{\le }\right)\to \mathrm{ordTop}\left(o\right)=\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)$$
23	22	opeq2d	$$⊢\left(f=F\wedge o=\underset{\dot{}}{\le }\right)\to ⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(o\right)⟩=⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)⟩$$
24	20 23	preq12d	$$⊢\left(f=F\wedge o=\underset{\dot{}}{\le }\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},f⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(o\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)⟩\right\}$$
25	21	opeq2d	$$⊢\left(f=F\wedge o=\underset{\dot{}}{\le }\right)\to ⟨{\le }_{\mathrm{ndx}},o⟩=⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩$$
26		id	$$⊢f=F\to f=F$$
27		rabeq	$$⊢f=F\to \left\{y\in f|y\cap x=\varnothing \right\}=\left\{y\in F|y\cap x=\varnothing \right\}$$
28	27	unieqd	$$⊢f=F\to \bigcup \left\{y\in f|y\cap x=\varnothing \right\}=\bigcup \left\{y\in F|y\cap x=\varnothing \right\}$$
29	26 28	mpteq12dv	$$⊢f=F\to \left(x\in f⟼\bigcup \left\{y\in f|y\cap x=\varnothing \right\}\right)=\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)$$
30	29	adantr	$$⊢\left(f=F\wedge o=\underset{\dot{}}{\le }\right)\to \left(x\in f⟼\bigcup \left\{y\in f|y\cap x=\varnothing \right\}\right)=\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)$$
31	30	opeq2d	$$⊢\left(f=F\wedge o=\underset{\dot{}}{\le }\right)\to ⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in f⟼\bigcup \left\{y\in f|y\cap x=\varnothing \right\}\right)⟩=⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩$$
32	25 31	preq12d	$$⊢\left(f=F\wedge o=\underset{\dot{}}{\le }\right)\to \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\}=\left\{⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}$$
33	24 32	uneq12d	$$⊢\left(f=F\wedge o=\underset{\dot{}}{\le }\right)\to \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\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}$$
34	14 18 33	csbied2	$$⊢f=F\to ⦋\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)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}$$
35		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)$$
36		prex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)⟩\right\}\in \mathrm{V}$$
37		prex	$$⊢\left\{⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}\in \mathrm{V}$$
38	36 37	unex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}\in \mathrm{V}$$
39	34 35 38	fvmpt	$$⊢F\in \mathrm{V}\to \mathrm{toInc}\left(F\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}$$
40	1 39	eqtrid	$$⊢F\in \mathrm{V}\to I=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}$$
41	3 40	syl	$$⊢F\in V\to I=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}$$