Metamath Proof Explorer


Theorem chunssji

Description: Union is smaller than CH join. (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 AC
chjcl.2 BC
Assertion chunssji ABAB

Proof

Step Hyp Ref Expression
1 ch0le.1 AC
2 chjcl.2 BC
3 1 chshii AS
4 2 chshii BS
5 3 4 shunssji ABAB