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 {\mathbf{S}}_{\mathscr{H}}$$
	shincl.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	shunssji	$$⊢A\cup B\subseteq A{\vee }_{\mathscr{H}}B$$

Proof

Step	Hyp	Ref	Expression
1		shincl.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
2		shincl.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
3	1	shssii	$$⊢A\subseteq \mathscr{H}$$
4	2	shssii	$$⊢B\subseteq \mathscr{H}$$
5	3 4	unssi	$$⊢A\cup B\subseteq \mathscr{H}$$
6		ococss	$$⊢A\cup B\subseteq \mathscr{H}\to A\cup B\subseteq \perp \left(\perp \left(A\cup B\right)\right)$$
7	5 6	ax-mp	$$⊢A\cup B\subseteq \perp \left(\perp \left(A\cup B\right)\right)$$
8		shjval	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to A{\vee }_{\mathscr{H}}B=\perp \left(\perp \left(A\cup B\right)\right)$$
9	1 2 8	mp2an	$$⊢A{\vee }_{\mathscr{H}}B=\perp \left(\perp \left(A\cup B\right)\right)$$
10	7 9	sseqtrri	$$⊢A\cup B\subseteq A{\vee }_{\mathscr{H}}B$$