Theorem hashunif

Description: The cardinality of a disjoint finite union of finite sets. Cf. hashuni . (Contributed by Thierry Arnoux, 17-Feb-2017)

	Ref	Expression
Hypotheses	hashiunf.1	|- F/ x ph
	hashiunf.3	|- ( ph -> A e. Fin )
	hashunif.4	|- ( ph -> A C_ Fin )
	hashunif.5	|- ( ph -> Disj_ x e. A x )
Assertion	hashunif	|- ( ph -> ( # ` U. A ) = sum_ x e. A ( # ` x ) )

Proof

Step	Hyp	Ref	Expression
1		hashiunf.1	|- F/ x ph
2		hashiunf.3	|- ( ph -> A e. Fin )
3		hashunif.4	|- ( ph -> A C_ Fin )
4		hashunif.5	|- ( ph -> Disj_ x e. A x )
5		uniiun	|- U. A = U_ x e. A x
6	5	fveq2i	|- ( # ` U. A ) = ( # ` U_ x e. A x )
7	3	sselda	|- ( ( ph /\ y e. A ) -> y e. Fin )
8		id	|- ( x = y -> x = y )
9	8	cbvdisjv	|- ( Disj_ x e. A x <-> Disj_ y e. A y )
10	4 9	sylib	|- ( ph -> Disj_ y e. A y )
11	2 7 10	hashiun	|- ( ph -> ( # ` U_ y e. A y ) = sum_ y e. A ( # ` y ) )
12	8	cbviunv	|- U_ x e. A x = U_ y e. A y
13	12	a1i	|- ( ph -> U_ x e. A x = U_ y e. A y )
14	13	fveq2d	|- ( ph -> ( # ` U_ x e. A x ) = ( # ` U_ y e. A y ) )
15		fveq2	|- ( x = y -> ( # ` x ) = ( # ` y ) )
16	15	cbvsumv	|- sum_ x e. A ( # ` x ) = sum_ y e. A ( # ` y )
17	16	a1i	|- ( ph -> sum_ x e. A ( # ` x ) = sum_ y e. A ( # ` y ) )
18	11 14 17	3eqtr4d	|- ( ph -> ( # ` U_ x e. A x ) = sum_ x e. A ( # ` x ) )
19	6 18	syl5eq	|- ( ph -> ( # ` U. A ) = sum_ x e. A ( # ` x ) )