Theorem hashuni

Description: The cardinality of a disjoint union. (Contributed by Mario Carneiro, 24-Jan-2015)

	Ref	Expression
Hypotheses	hashuni.1	|- ( ph -> A e. Fin )
	hashuni.2	|- ( ph -> A C_ Fin )
	hashuni.3	|- ( ph -> Disj_ x e. A x )
Assertion	hashuni	|- ( ph -> ( # ` U. A ) = sum_ x e. A ( # ` x ) )

Proof

Step	Hyp	Ref	Expression
1		hashuni.1	|- ( ph -> A e. Fin )
2		hashuni.2	|- ( ph -> A C_ Fin )
3		hashuni.3	|- ( ph -> Disj_ x e. A x )
4		uniiun	|- U. A = U_ x e. A x
5	4	fveq2i	|- ( # ` U. A ) = ( # ` U_ x e. A x )
6	2	sselda	|- ( ( ph /\ x e. A ) -> x e. Fin )
7	1 6 3	hashiun	|- ( ph -> ( # ` U_ x e. A x ) = sum_ x e. A ( # ` x ) )
8	5 7	eqtrid	|- ( ph -> ( # ` U. A ) = sum_ x e. A ( # ` x ) )