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	⊢ 𝐴 ∈ Sℋ
	shincl.2	⊢ 𝐵 ∈ Sℋ
Assertion	shunssji	⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		shincl.1	⊢ 𝐴 ∈ Sℋ
2		shincl.2	⊢ 𝐵 ∈ Sℋ
3	1	shssii	⊢ 𝐴 ⊆ ℋ
4	2	shssii	⊢ 𝐵 ⊆ ℋ
5	3 4	unssi	⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ℋ
6		ococss	⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ ℋ → ( 𝐴 ∪ 𝐵 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
7	5 6	ax-mp	⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) )
8		shjval	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
9	1 2 8	mp2an	⊢ ( 𝐴 ∨ℋ 𝐵 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) )
10	7 9	sseqtrri	⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 )