Theorem ipobas

Description: Base set of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015) (Revised by Mario Carneiro, 25-Oct-2015)

	Ref	Expression
Hypothesis	ipoval.i	$$⊢I=\mathrm{toInc}\left(F\right)$$
Assertion	ipobas	$$⊢F\in V\to F={\mathrm{Base}}_I$$

Proof

Step	Hyp	Ref	Expression
1		ipoval.i	$$⊢I=\mathrm{toInc}\left(F\right)$$
2		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⟩$$
3		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
4		snsspr1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩\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\}$$
5		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\}$$
6	4 5	sstri	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},F⟩\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\}$$
7	2 3 6	strfv	$$⊢F\in V\to F={\mathrm{Base}}_{\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)}$$
8		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\}$$
9	1 8	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\}$$
10	9	fveq2d	$$⊢F\in V\to {\mathrm{Base}}_I={\mathrm{Base}}_{\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	7 10	eqtr4d	$$⊢F\in V\to F={\mathrm{Base}}_I$$