sshjcl

Description: Closure of join for subsets of Hilbert space. (Contributed by NM, 1-Nov-2000) (New usage is discouraged.)

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

Step	Hyp	Ref	Expression
1		sshjval	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to A \lor_{ℋ} B = ⊥ (⊥ (A \cup B))$
2		unss	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \leftrightarrow A \cup B \subseteq ℋ$
3		ocss	$⊢ A \cup B \subseteq ℋ \to ⊥ (A \cup B) \subseteq ℋ$
4		occl	$⊢ ⊥ (A \cup B) \subseteq ℋ \to ⊥ (⊥ (A \cup B)) \in C_{ℋ}$
5	3 4	syl	$⊢ A \cup B \subseteq ℋ \to ⊥ (⊥ (A \cup B)) \in C_{ℋ}$
6	2 5	sylbi	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to ⊥ (⊥ (A \cup B)) \in C_{ℋ}$
7	1 6	eqeltrd	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to A \lor_{ℋ} B \in C_{ℋ}$

Metamath Proof Explorer