Metamath Proof Explorer


Theorem unidom

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

Proof

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