chsupss

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

		Ref	Expression
	Assertion	chsupss	$⊢ (A \subseteq C_{ℋ} \land B \subseteq C_{ℋ}) \to (A \subseteq B \to ⋁_{ℋ} (A) \subseteq ⋁_{ℋ} (B))$

Step	Hyp	Ref	Expression
1		chsspwh	$⊢ C_{ℋ} \subseteq 𝒫 ℋ$
2		sstr2	$⊢ A \subseteq C_{ℋ} \to (C_{ℋ} \subseteq 𝒫 ℋ \to A \subseteq 𝒫 ℋ)$
3	1 2	mpi	$⊢ A \subseteq C_{ℋ} \to A \subseteq 𝒫 ℋ$
4		sstr2	$⊢ B \subseteq C_{ℋ} \to (C_{ℋ} \subseteq 𝒫 ℋ \to B \subseteq 𝒫 ℋ)$
5	1 4	mpi	$⊢ B \subseteq C_{ℋ} \to B \subseteq 𝒫 ℋ$
6		hsupss	$⊢ (A \subseteq 𝒫 ℋ \land B \subseteq 𝒫 ℋ) \to (A \subseteq B \to ⋁_{ℋ} (A) \subseteq ⋁_{ℋ} (B))$
7	3 5 6	syl2an	$⊢ (A \subseteq C_{ℋ} \land B \subseteq C_{ℋ}) \to (A \subseteq B \to ⋁_{ℋ} (A) \subseteq ⋁_{ℋ} (B))$

Metamath Proof Explorer