Theorem ipotset

Description: Topology of the inclusion poset. (Contributed by Mario Carneiro, 24-Oct-2015)

	Ref	Expression
Hypotheses	ipoval.i	$$⊢I=\mathrm{toInc}\left(F\right)$$
	ipole.l	$$⊢\underset{\dot{}}{\le }={\le }_I$$
Assertion	ipotset	$$⊢F\in V\to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)=\mathrm{TopSet}\left(I\right)$$

Proof

Step	Hyp	Ref	Expression
1		ipoval.i	$$⊢I=\mathrm{toInc}\left(F\right)$$
2		ipole.l	$$⊢\underset{\dot{}}{\le }={\le }_I$$
3		fvex	$$⊢\mathrm{ordTop}\left(\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\right)\in \mathrm{V}$$
4		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⟩$$
5		tsetid	$$⊢\mathrm{TopSet}=\mathrm{Slot}\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
6		snsspr2	$$⊢\left\{⟨\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\}\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\}$$
7		ssun1	$$⊢\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\}\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\}$$
8	6 7	sstri	$$⊢\left\{⟨\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\}\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\}$$
9	4 5 8	strfv	$$⊢\mathrm{ordTop}\left(\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\right)\in \mathrm{V}\to \mathrm{ordTop}\left(\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\right)=\mathrm{TopSet}\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)$$
10	3 9	ax-mp	$$⊢\mathrm{ordTop}\left(\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\right)=\mathrm{TopSet}\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)$$
11	1	ipolerval	$$⊢F\in V\to \left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}={\le }_I$$
12	11 2	syl6reqr	$$⊢F\in V\to \underset{\dot{}}{\le }=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}$$
13	12	fveq2d	$$⊢F\in V\to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)=\mathrm{ordTop}\left(\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}\right)$$
14		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\}$$
15	1 14	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\}$$
16	15	fveq2d	$$⊢F\in V\to \mathrm{TopSet}\left(I\right)=\mathrm{TopSet}\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)$$
17	10 13 16	3eqtr4a	$$⊢F\in V\to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)=\mathrm{TopSet}\left(I\right)$$