Metamath Proof Explorer

Theorem cardiun

Description: The indexed union of a set of cardinals is a cardinal. (Contributed by NM, 3-Nov-2003)

Ref Expression
Assertion cardiun 
|- ( A e. V -> ( A. x e. A ( card ` B ) = B -> ( card ` U_ x e. A B ) = U_ x e. A B ) )

Proof

Step Hyp Ref Expression
1 abrexexg 
 |-  ( A e. V -> { z | E. x e. A z = ( card ` B ) } e. _V )
2 vex 
 |-  y e. _V
3 eqeq1 
 |-  ( z = y -> ( z = ( card ` B ) <-> y = ( card ` B ) ) )
4 3 rexbidv 
 |-  ( z = y -> ( E. x e. A z = ( card ` B ) <-> E. x e. A y = ( card ` B ) ) )
5 2 4 elab 
 |-  ( y e. { z | E. x e. A z = ( card ` B ) } <-> E. x e. A y = ( card ` B ) )
6 cardidm 
 |-  ( card ` ( card ` B ) ) = ( card ` B )
7 fveq2 
 |-  ( y = ( card ` B ) -> ( card ` y ) = ( card ` ( card ` B ) ) )
8 id 
 |-  ( y = ( card ` B ) -> y = ( card ` B ) )
9 6 7 8 3eqtr4a 
 |-  ( y = ( card ` B ) -> ( card ` y ) = y )
10 9 rexlimivw 
 |-  ( E. x e. A y = ( card ` B ) -> ( card ` y ) = y )
11 5 10 sylbi 
 |-  ( y e. { z | E. x e. A z = ( card ` B ) } -> ( card ` y ) = y )
12 11 rgen 
 |-  A. y e. { z | E. x e. A z = ( card ` B ) } ( card ` y ) = y
13 carduni 
 |-  ( { z | E. x e. A z = ( card ` B ) } e. _V -> ( A. y e. { z | E. x e. A z = ( card ` B ) } ( card ` y ) = y -> ( card ` U. { z | E. x e. A z = ( card ` B ) } ) = U. { z | E. x e. A z = ( card ` B ) } ) )
14 1 12 13 mpisyl 
 |-  ( A e. V -> ( card ` U. { z | E. x e. A z = ( card ` B ) } ) = U. { z | E. x e. A z = ( card ` B ) } )
15 fvex 
 |-  ( card ` B ) e. _V
16 15 dfiun2 
 |-  U_ x e. A ( card ` B ) = U. { z | E. x e. A z = ( card ` B ) }
17 16 fveq2i 
 |-  ( card ` U_ x e. A ( card ` B ) ) = ( card ` U. { z | E. x e. A z = ( card ` B ) } )
18 14 17 16 3eqtr4g 
 |-  ( A e. V -> ( card ` U_ x e. A ( card ` B ) ) = U_ x e. A ( card ` B ) )
19 18 adantr 
 |-  ( ( A e. V /\ A. x e. A ( card ` B ) = B ) -> ( card ` U_ x e. A ( card ` B ) ) = U_ x e. A ( card ` B ) )
20 iuneq2 
 |-  ( A. x e. A ( card ` B ) = B -> U_ x e. A ( card ` B ) = U_ x e. A B )
21 20 adantl 
 |-  ( ( A e. V /\ A. x e. A ( card ` B ) = B ) -> U_ x e. A ( card ` B ) = U_ x e. A B )
22 21 fveq2d 
 |-  ( ( A e. V /\ A. x e. A ( card ` B ) = B ) -> ( card ` U_ x e. A ( card ` B ) ) = ( card ` U_ x e. A B ) )
23 19 22 21 3eqtr3d 
 |-  ( ( A e. V /\ A. x e. A ( card ` B ) = B ) -> ( card ` U_ x e. A B ) = U_ x e. A B )
24 23 ex 
 |-  ( A e. V -> ( A. x e. A ( card ` B ) = B -> ( card ` U_ x e. A B ) = U_ x e. A B ) )