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 e. SH
shincl.2
|- B e. SH
Assertion shunssji
|- ( A u. B ) C_ ( A vH B )

Proof

Step Hyp Ref Expression
1 shincl.1
 |-  A e. SH
2 shincl.2
 |-  B e. SH
3 1 shssii
 |-  A C_ ~H
4 2 shssii
 |-  B C_ ~H
5 3 4 unssi
 |-  ( A u. B ) C_ ~H
6 ococss
 |-  ( ( A u. B ) C_ ~H -> ( A u. B ) C_ ( _|_ ` ( _|_ ` ( A u. B ) ) ) )
7 5 6 ax-mp
 |-  ( A u. B ) C_ ( _|_ ` ( _|_ ` ( A u. B ) ) )
8 shjval
 |-  ( ( A e. SH /\ B e. SH ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) )
9 1 2 8 mp2an
 |-  ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) )
10 7 9 sseqtrri
 |-  ( A u. B ) C_ ( A vH B )