Metamath Proof Explorer

Theorem cardinfima

Description: If a mapping to cardinals has an infinite value, then the union of its image is an infinite cardinal. Corollary 11.17 of TakeutiZaring p. 104. (Contributed by NM, 4-Nov-2004)

Ref Expression
Assertion cardinfima 
|- ( A e. B -> ( ( F : A --> ( _om u. ran aleph ) /\ E. x e. A ( F ` x ) e. ran aleph ) -> U. ( F " A ) e. ran aleph ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. B -> A e. _V )
2 isinfcard 
 |-  ( ( _om C_ ( F ` x ) /\ ( card ` ( F ` x ) ) = ( F ` x ) ) <-> ( F ` x ) e. ran aleph )
3 2 bicomi 
 |-  ( ( F ` x ) e. ran aleph <-> ( _om C_ ( F ` x ) /\ ( card ` ( F ` x ) ) = ( F ` x ) ) )
4 3 simplbi 
 |-  ( ( F ` x ) e. ran aleph -> _om C_ ( F ` x ) )
5 ffn 
 |-  ( F : A --> ( _om u. ran aleph ) -> F Fn A )
6 fnfvelrn 
 |-  ( ( F Fn A /\ x e. A ) -> ( F ` x ) e. ran F )
7 6 ex 
 |-  ( F Fn A -> ( x e. A -> ( F ` x ) e. ran F ) )
8 fnima 
 |-  ( F Fn A -> ( F " A ) = ran F )
9 8 eleq2d 
 |-  ( F Fn A -> ( ( F ` x ) e. ( F " A ) <-> ( F ` x ) e. ran F ) )
10 7 9 sylibrd 
 |-  ( F Fn A -> ( x e. A -> ( F ` x ) e. ( F " A ) ) )
11 elssuni 
 |-  ( ( F ` x ) e. ( F " A ) -> ( F ` x ) C_ U. ( F " A ) )
12 10 11 syl6 
 |-  ( F Fn A -> ( x e. A -> ( F ` x ) C_ U. ( F " A ) ) )
13 12 imp 
 |-  ( ( F Fn A /\ x e. A ) -> ( F ` x ) C_ U. ( F " A ) )
14 5 13 sylan 
 |-  ( ( F : A --> ( _om u. ran aleph ) /\ x e. A ) -> ( F ` x ) C_ U. ( F " A ) )
15 4 14 sylan9ssr 
 |-  ( ( ( F : A --> ( _om u. ran aleph ) /\ x e. A ) /\ ( F ` x ) e. ran aleph ) -> _om C_ U. ( F " A ) )
16 15 anasss 
 |-  ( ( F : A --> ( _om u. ran aleph ) /\ ( x e. A /\ ( F ` x ) e. ran aleph ) ) -> _om C_ U. ( F " A ) )
17 16 a1i 
 |-  ( A e. _V -> ( ( F : A --> ( _om u. ran aleph ) /\ ( x e. A /\ ( F ` x ) e. ran aleph ) ) -> _om C_ U. ( F " A ) ) )
18 carduniima 
 |-  ( A e. _V -> ( F : A --> ( _om u. ran aleph ) -> U. ( F " A ) e. ( _om u. ran aleph ) ) )
19 iscard3 
 |-  ( ( card ` U. ( F " A ) ) = U. ( F " A ) <-> U. ( F " A ) e. ( _om u. ran aleph ) )
20 18 19 imbitrrdi 
 |-  ( A e. _V -> ( F : A --> ( _om u. ran aleph ) -> ( card ` U. ( F " A ) ) = U. ( F " A ) ) )
21 20 adantrd 
 |-  ( A e. _V -> ( ( F : A --> ( _om u. ran aleph ) /\ ( x e. A /\ ( F ` x ) e. ran aleph ) ) -> ( card ` U. ( F " A ) ) = U. ( F " A ) ) )
22 17 21 jcad 
 |-  ( A e. _V -> ( ( F : A --> ( _om u. ran aleph ) /\ ( x e. A /\ ( F ` x ) e. ran aleph ) ) -> ( _om C_ U. ( F " A ) /\ ( card ` U. ( F " A ) ) = U. ( F " A ) ) ) )
23 isinfcard 
 |-  ( ( _om C_ U. ( F " A ) /\ ( card ` U. ( F " A ) ) = U. ( F " A ) ) <-> U. ( F " A ) e. ran aleph )
24 22 23 imbitrdi 
 |-  ( A e. _V -> ( ( F : A --> ( _om u. ran aleph ) /\ ( x e. A /\ ( F ` x ) e. ran aleph ) ) -> U. ( F " A ) e. ran aleph ) )
25 24 exp4d 
 |-  ( A e. _V -> ( F : A --> ( _om u. ran aleph ) -> ( x e. A -> ( ( F ` x ) e. ran aleph -> U. ( F " A ) e. ran aleph ) ) ) )
26 25 imp 
 |-  ( ( A e. _V /\ F : A --> ( _om u. ran aleph ) ) -> ( x e. A -> ( ( F ` x ) e. ran aleph -> U. ( F " A ) e. ran aleph ) ) )
27 26 rexlimdv 
 |-  ( ( A e. _V /\ F : A --> ( _om u. ran aleph ) ) -> ( E. x e. A ( F ` x ) e. ran aleph -> U. ( F " A ) e. ran aleph ) )
28 27 expimpd 
 |-  ( A e. _V -> ( ( F : A --> ( _om u. ran aleph ) /\ E. x e. A ( F ` x ) e. ran aleph ) -> U. ( F " A ) e. ran aleph ) )
29 1 28 syl 
 |-  ( A e. B -> ( ( F : A --> ( _om u. ran aleph ) /\ E. x e. A ( F ` x ) e. ran aleph ) -> U. ( F " A ) e. ran aleph ) )