Theorem carduniima

Description: The union of the image of a mapping to cardinals is a cardinal. Proposition 11.16 of TakeutiZaring p. 104. (Contributed by NM, 4-Nov-2004)

	Ref	Expression
Assertion	carduniima	|- ( A e. B -> ( F : A --> ( _om u. ran aleph ) -> U. ( F " A ) e. ( _om u. ran aleph ) ) )

Proof

Step	Hyp	Ref	Expression
1		ffun	|- ( F : A --> ( _om u. ran aleph ) -> Fun F )
2		funimaexg	|- ( ( Fun F /\ A e. B ) -> ( F " A ) e. _V )
3	1 2	sylan	|- ( ( F : A --> ( _om u. ran aleph ) /\ A e. B ) -> ( F " A ) e. _V )
4	3	expcom	|- ( A e. B -> ( F : A --> ( _om u. ran aleph ) -> ( F " A ) e. _V ) )
5		fimass	|- ( F : A --> ( _om u. ran aleph ) -> ( F " A ) C_ ( _om u. ran aleph ) )
6	5	sseld	|- ( F : A --> ( _om u. ran aleph ) -> ( x e. ( F " A ) -> x e. ( _om u. ran aleph ) ) )
7		iscard3	|- ( ( card ` x ) = x <-> x e. ( _om u. ran aleph ) )
8	6 7	imbitrrdi	|- ( F : A --> ( _om u. ran aleph ) -> ( x e. ( F " A ) -> ( card ` x ) = x ) )
9	8	ralrimiv	|- ( F : A --> ( _om u. ran aleph ) -> A. x e. ( F " A ) ( card ` x ) = x )
10		carduni	|- ( ( F " A ) e. _V -> ( A. x e. ( F " A ) ( card ` x ) = x -> ( card ` U. ( F " A ) ) = U. ( F " A ) ) )
11	9 10	syl5	|- ( ( F " A ) e. _V -> ( F : A --> ( _om u. ran aleph ) -> ( card ` U. ( F " A ) ) = U. ( F " A ) ) )
12	4 11	syli	|- ( A e. B -> ( F : A --> ( _om u. ran aleph ) -> ( card ` U. ( F " A ) ) = U. ( F " A ) ) )
13		iscard3	|- ( ( card ` U. ( F " A ) ) = U. ( F " A ) <-> U. ( F " A ) e. ( _om u. ran aleph ) )
14	12 13	imbitrdi	|- ( A e. B -> ( F : A --> ( _om u. ran aleph ) -> U. ( F " A ) e. ( _om u. ran aleph ) ) )