Theorem ipolerval

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

	Ref	Expression
Hypothesis	ipoval.i	$$⊢I=\mathrm{toInc}\left(F\right)$$
Assertion	ipolerval	$$⊢F\in V\to \left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}={\le }_I$$

Proof

Step	Hyp	Ref	Expression
1		ipoval.i	$$⊢I=\mathrm{toInc}\left(F\right)$$
2		simpl	$$⊢\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\to \left\{x,y\right\}\subseteq F$$
3		vex	$$⊢x\in \mathrm{V}$$
4		vex	$$⊢y\in \mathrm{V}$$
5	3 4	prss	$$⊢\left(x\in F\wedge y\in F\right)\leftrightarrow \left\{x,y\right\}\subseteq F$$
6	2 5	sylibr	$$⊢\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\to \left(x\in F\wedge y\in F\right)$$
7	6	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\}$$
8		df-xp	$$⊢F\times F=\left\{⟨x,y⟩|\left(x\in F\wedge y\in F\right)\right\}$$
9	7 8	sseqtrri	$$⊢\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\subseteq F\times F$$
10		sqxpexg	$$⊢F\in V\to F\times F\in \mathrm{V}$$
11		ssexg	$$⊢\left(\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\subseteq F\times F\wedge F\times F\in \mathrm{V}\right)\to \left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\in \mathrm{V}$$
12	9 10 11	sylancr	$$⊢F\in V\to \left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\in \mathrm{V}$$
13		ipostr	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}\right)\mathrm{Struct}⟨1,11⟩$$
14		pleid	$$⊢\mathrm{le}=\mathrm{Slot}{\le }_{\mathrm{ndx}}$$
15		snsspr1	$$⊢\left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}⟩\right\}\subseteq \left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}$$
16		ssun2	$$⊢\left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}$$
17	15 16	sstri	$$⊢\left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}$$
18	13 14 17	strfv	$$⊢\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\in \mathrm{V}\to \left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}={\le }_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}\right)}$$
19	12 18	syl	$$⊢F\in V\to \left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}={\le }_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}\right)}$$
20		eqid	$$⊢\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\}$$
21	1 20	ipoval	$$⊢F\in V\to I=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}$$
22	21	fveq2d	$$⊢F\in V\to {\le }_I={\le }_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\right)⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\left(x\in F⟼\bigcup \left\{y\in F|y\cap x=\varnothing \right\}\right)⟩\right\}\right)}$$
23	19 22	eqtr4d	$$⊢F\in V\to \left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}={\le }_I$$