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 ) ) |