Theorem chsupid

Description: A subspace is the supremum of all smaller subspaces. (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

	Ref	Expression
Assertion	chsupid	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to {\bigvee }_{\mathscr{H}}\left(\left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		ssrab2	$$⊢\left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
2		chsupval2	$$⊢\left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}\to {\bigvee }_{\mathscr{H}}\left(\left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\right)=\bigcap \left\{y\in {\mathbf{C}}_{\mathscr{H}}|\bigcup \left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\subseteq y\right\}$$
3	1 2	ax-mp	$$⊢{\bigvee }_{\mathscr{H}}\left(\left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\right)=\bigcap \left\{y\in {\mathbf{C}}_{\mathscr{H}}|\bigcup \left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\subseteq y\right\}$$
4		unimax	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \bigcup \left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}=A$$
5	4	sseq1d	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(\bigcup \left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\subseteq y\leftrightarrow A\subseteq y\right)$$
6	5	rabbidv	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left\{y\in {\mathbf{C}}_{\mathscr{H}}|\bigcup \left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\subseteq y\right\}=\left\{y\in {\mathbf{C}}_{\mathscr{H}}|A\subseteq y\right\}$$
7	6	inteqd	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \bigcap \left\{y\in {\mathbf{C}}_{\mathscr{H}}|\bigcup \left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\subseteq y\right\}=\bigcap \left\{y\in {\mathbf{C}}_{\mathscr{H}}|A\subseteq y\right\}$$
8		intmin	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \bigcap \left\{y\in {\mathbf{C}}_{\mathscr{H}}|A\subseteq y\right\}=A$$
9	7 8	eqtrd	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \bigcap \left\{y\in {\mathbf{C}}_{\mathscr{H}}|\bigcup \left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\subseteq y\right\}=A$$
10	3 9	syl5eq	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to {\bigvee }_{\mathscr{H}}\left(\left\{x\in {\mathbf{C}}_{\mathscr{H}}|x\subseteq A\right\}\right)=A$$