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 S
shincl.2 B S
Assertion shunssji A B A B

Proof

Step Hyp Ref Expression
1 shincl.1 A S
2 shincl.2 B S
3 1 shssii A
4 2 shssii B
5 3 4 unssi A B
6 ococss A B A B A B
7 5 6 ax-mp A B A B
8 shjval A S B S A B = A B
9 1 2 8 mp2an A B = A B
10 7 9 sseqtrri A B A B