This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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