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		simpl	$$⊢\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\to \left\{x,y\right\}\subseteq f$$
7		vex	$$⊢x\in \mathrm{V}$$
8		vex	$$⊢y\in \mathrm{V}$$
9	7 8	prss	$$⊢\left(x\in f\wedge y\in f\right)\leftrightarrow \left\{x,y\right\}\subseteq f$$
10	6 9	sylibr	$$⊢\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\to \left(x\in f\wedge y\in f\right)$$
11	10	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\}$$
12		df-xp	$$⊢f\times f=\left\{⟨x,y⟩|\left(x\in f\wedge y\in f\right)\right\}$$
13	11 12	sseqtrri	$$⊢\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\right\}\subseteq f\times f$$
14	5 13	ssexi	$$⊢\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\right\}\in \mathrm{V}$$
15	14	a1i	$$⊢f=F\to \left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\right\}\in \mathrm{V}$$
16		sseq2	$$⊢f=F\to \left(\left\{x,y\right\}\subseteq f\leftrightarrow \left\{x,y\right\}\subseteq F\right)$$
17	16	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)$$
18	17	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\}$$
19	18 2	syl6eqr	$$⊢f=F\to \left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq f\wedge x\subseteq y\right)\right\}=\underset{\dot{}}{\le }$$
20		simpl	$$⊢\left(f=F\wedge o=\underset{\dot{}}{\le }\right)\to f=F$$
21	20	opeq2d	$$⊢\left(f=F\wedge o=\underset{\dot{}}{\le }\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},f⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩$$
22		simpr	$$⊢\left(f=F\wedge o=\underset{\dot{}}{\le }\right)\to o=\underset{\dot{}}{\le }$$
23	22	fveq2d	$$⊢\left(f=F\wedge o=\underset{\dot{}}{\le }\right)\to \mathrm{ordTop}\left(o\right)=\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)$$
24	23	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)⟩$$
25	21 24	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\}$$
26	22	opeq2d	$$⊢\left(f=F\wedge o=\underset{\dot{}}{\le }\right)\to ⟨{\le }_{\mathrm{ndx}},o⟩=⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩$$
27		id	$$⊢f=F\to f=F$$
28		rabeq	$$⊢f=F\to \left\{y\in f|y\cap x=\varnothing \right\}=\left\{y\in F|y\cap x=\varnothing \right\}$$
29	28	unieqd	$$⊢f=F\to \bigcup \left\{y\in f|y\cap x=\varnothing \right\}=\bigcup \left\{y\in F|y\cap x=\varnothing \right\}$$
30	27 29	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)$$
31	30	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)$$
32	31	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)⟩$$
33	26 32	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\}$$
34	25 33	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\}$$
35	15 19 34	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\}$$
36		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)$$
37		prex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)⟩\right\}\in \mathrm{V}$$
38		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}$$
39	37 38	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}$$
40	35 36 39	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\}$$
41	1 40	syl5eq	$$⊢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\}$$
42	3 41	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\}$$