Theorem chsupsn

Description: Value of supremum of subset of CH on a singleton. (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		snssi	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left\{A\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
2		chsupval2	$$⊢\left\{A\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}\to {\bigvee }_{\mathscr{H}}\left(\left\{A\right\}\right)=\bigcap \left\{x\in {\mathbf{C}}_{\mathscr{H}}|\bigcup \left\{A\right\}\subseteq x\right\}$$
3	1 2	syl	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to {\bigvee }_{\mathscr{H}}\left(\left\{A\right\}\right)=\bigcap \left\{x\in {\mathbf{C}}_{\mathscr{H}}|\bigcup \left\{A\right\}\subseteq x\right\}$$
4		unisng	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \bigcup \left\{A\right\}=A$$
5		eqimss	$$⊢\bigcup \left\{A\right\}=A\to \bigcup \left\{A\right\}\subseteq A$$
6	4 5	syl	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \bigcup \left\{A\right\}\subseteq A$$
7	6	ancli	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \bigcup \left\{A\right\}\subseteq A\right)$$
8		sseq2	$$⊢x=A\to \left(\bigcup \left\{A\right\}\subseteq x\leftrightarrow \bigcup \left\{A\right\}\subseteq A\right)$$
9	8	elrab	$$⊢A\in \left\{x\in {\mathbf{C}}_{\mathscr{H}}|\bigcup \left\{A\right\}\subseteq x\right\}\leftrightarrow \left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \bigcup \left\{A\right\}\subseteq A\right)$$
10	7 9	sylibr	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A\in \left\{x\in {\mathbf{C}}_{\mathscr{H}}|\bigcup \left\{A\right\}\subseteq x\right\}$$
11		intss1	$$⊢A\in \left\{x\in {\mathbf{C}}_{\mathscr{H}}|\bigcup \left\{A\right\}\subseteq x\right\}\to \bigcap \left\{x\in {\mathbf{C}}_{\mathscr{H}}|\bigcup \left\{A\right\}\subseteq x\right\}\subseteq A$$
12	10 11	syl	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \bigcap \left\{x\in {\mathbf{C}}_{\mathscr{H}}|\bigcup \left\{A\right\}\subseteq x\right\}\subseteq A$$
13		ssintub	$$⊢\bigcup \left\{A\right\}\subseteq \bigcap \left\{x\in {\mathbf{C}}_{\mathscr{H}}|\bigcup \left\{A\right\}\subseteq x\right\}$$
14	4 13	eqsstrrdi	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A\subseteq \bigcap \left\{x\in {\mathbf{C}}_{\mathscr{H}}|\bigcup \left\{A\right\}\subseteq x\right\}$$
15	12 14	eqssd	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \bigcap \left\{x\in {\mathbf{C}}_{\mathscr{H}}|\bigcup \left\{A\right\}\subseteq x\right\}=A$$
16	3 15	eqtrd	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to {\bigvee }_{\mathscr{H}}\left(\left\{A\right\}\right)=A$$