Description: An upper bound for the cardinality of a union. Theorem 10.47 of TakeutiZaring p. 98. (Contributed by NM, 25-Mar-2006) (Proof shortened by Mario Carneiro, 1-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | unidom | |- ( ( A e. V /\ A. x e. A x ~<_ B ) -> U. A ~<_ ( A X. B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniiun | |- U. A = U_ x e. A x |
|
2 | iundom | |- ( ( A e. V /\ A. x e. A x ~<_ B ) -> U_ x e. A x ~<_ ( A X. B ) ) |
|
3 | 1 2 | eqbrtrid | |- ( ( A e. V /\ A. x e. A x ~<_ B ) -> U. A ~<_ ( A X. B ) ) |