Theorem unilbss

Description: Superclass of the greatest lower bound. A dual statement of ssintub . (Contributed by Zhi Wang, 29-Sep-2024)

	Ref	Expression
Assertion	unilbss	$$⊢\bigcup \left\{x\in B|x\subseteq A\right\}\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		unissb	$$⊢\bigcup \left\{x\in B|x\subseteq A\right\}\subseteq A\leftrightarrow \forall y\in \left\{x\in B|x\subseteq A\right\}y\subseteq A$$
2		sseq1	$$⊢x=y\to \left(x\subseteq A\leftrightarrow y\subseteq A\right)$$
3	2	elrab	$$⊢y\in \left\{x\in B|x\subseteq A\right\}\leftrightarrow \left(y\in B\wedge y\subseteq A\right)$$
4	3	simprbi	$$⊢y\in \left\{x\in B|x\subseteq A\right\}\to y\subseteq A$$
5	1 4	mprgbir	$$⊢\bigcup \left\{x\in B|x\subseteq A\right\}\subseteq A$$