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 syl6ibr
 |-  ( 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 syl6ib
 |-  ( 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 ) )