chlub

Description: Hilbert lattice join is the least upper bound of two elements. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	chlub	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to ((A \subseteq C \land B \subseteq C) \leftrightarrow A \lor_{ℋ} B \subseteq C)$

Step	Hyp	Ref	Expression
1		chsh	$⊢ A \in C_{ℋ} \to A \in S_{ℋ}$
2		chsh	$⊢ B \in C_{ℋ} \to B \in S_{ℋ}$
3		shlub	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ} \land C \in C_{ℋ}) \to ((A \subseteq C \land B \subseteq C) \leftrightarrow A \lor_{ℋ} B \subseteq C)$
4	2 3	syl3an2	$⊢ (A \in S_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to ((A \subseteq C \land B \subseteq C) \leftrightarrow A \lor_{ℋ} B \subseteq C)$
5	1 4	syl3an1	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to ((A \subseteq C \land B \subseteq C) \leftrightarrow A \lor_{ℋ} B \subseteq C)$

Metamath Proof Explorer