This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem shunssji

Description: Union is smaller than Hilbert lattice join. (Contributed by NM, 11-Jun-2004) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	shincl.1	$⊢ A \in S_{ℋ}$
		shincl.2	$⊢ B \in S_{ℋ}$
	Assertion	shunssji	$⊢ A \cup B \subseteq A \lor_{ℋ} B$

Proof

Step	Hyp	Ref	Expression
1		shincl.1	$⊢ A \in S_{ℋ}$
2		shincl.2	$⊢ B \in S_{ℋ}$
3	1	shssii	$⊢ A \subseteq ℋ$
4	2	shssii	$⊢ B \subseteq ℋ$
5	3 4	unssi	$⊢ A \cup B \subseteq ℋ$
6		ococss	$⊢ A \cup B \subseteq ℋ \to A \cup B \subseteq ⊥ (⊥ (A \cup B))$
7	5 6	ax-mp	$⊢ A \cup B \subseteq ⊥ (⊥ (A \cup B))$
8		shjval	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to A \lor_{ℋ} B = ⊥ (⊥ (A \cup B))$
9	1 2 8	mp2an	$⊢ A \lor_{ℋ} B = ⊥ (⊥ (A \cup B))$
10	7 9	sseqtrri	$⊢ A \cup B \subseteq A \lor_{ℋ} B$