Theorem chsupss

Description: Subset relation for supremum of subset of CH . (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

	Ref	Expression
Assertion	chsupss	$$⊢\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge B\subseteq {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\subseteq B\to {\bigvee }_{\mathscr{H}}\left(A\right)\subseteq {\bigvee }_{\mathscr{H}}\left(B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		chsspwh	$$⊢{\mathbf{C}}_{\mathscr{H}}\subseteq 𝒫\mathscr{H}$$
2		sstr2	$$⊢A\subseteq {\mathbf{C}}_{\mathscr{H}}\to \left({\mathbf{C}}_{\mathscr{H}}\subseteq 𝒫\mathscr{H}\to A\subseteq 𝒫\mathscr{H}\right)$$
3	1 2	mpi	$$⊢A\subseteq {\mathbf{C}}_{\mathscr{H}}\to A\subseteq 𝒫\mathscr{H}$$
4		sstr2	$$⊢B\subseteq {\mathbf{C}}_{\mathscr{H}}\to \left({\mathbf{C}}_{\mathscr{H}}\subseteq 𝒫\mathscr{H}\to B\subseteq 𝒫\mathscr{H}\right)$$
5	1 4	mpi	$$⊢B\subseteq {\mathbf{C}}_{\mathscr{H}}\to B\subseteq 𝒫\mathscr{H}$$
6		hsupss	$$⊢\left(A\subseteq 𝒫\mathscr{H}\wedge B\subseteq 𝒫\mathscr{H}\right)\to \left(A\subseteq B\to {\bigvee }_{\mathscr{H}}\left(A\right)\subseteq {\bigvee }_{\mathscr{H}}\left(B\right)\right)$$
7	3 5 6	syl2an	$$⊢\left(A\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge B\subseteq {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\subseteq B\to {\bigvee }_{\mathscr{H}}\left(A\right)\subseteq {\bigvee }_{\mathscr{H}}\left(B\right)\right)$$