Metamath Proof Explorer

Theorem iunctb

Description: The countable union of countable sets is countable (indexed union version of unictb ). (Contributed by Mario Carneiro, 18-Jan-2014)

Ref Expression
Assertion iunctb 
|- ( ( A ~<_ _om /\ A. x e. A B ~<_ _om ) -> U_ x e. A B ~<_ _om )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U_ x e. A ( { x } X. B ) = U_ x e. A ( { x } X. B )
2 simpl 
 |-  ( ( A ~<_ _om /\ A. x e. A B ~<_ _om ) -> A ~<_ _om )
3 ctex 
 |-  ( A ~<_ _om -> A e. _V )
4 3 adantr 
 |-  ( ( A ~<_ _om /\ A. x e. A B ~<_ _om ) -> A e. _V )
5 ovex 
 |-  ( _om ^m B ) e. _V
6 5 rgenw 
 |-  A. x e. A ( _om ^m B ) e. _V
7 iunexg 
 |-  ( ( A e. _V /\ A. x e. A ( _om ^m B ) e. _V ) -> U_ x e. A ( _om ^m B ) e. _V )
8 4 6 7 sylancl 
 |-  ( ( A ~<_ _om /\ A. x e. A B ~<_ _om ) -> U_ x e. A ( _om ^m B ) e. _V )
9 acncc 
 |-  AC_ _om = _V
10 8 9 eleqtrrdi 
 |-  ( ( A ~<_ _om /\ A. x e. A B ~<_ _om ) -> U_ x e. A ( _om ^m B ) e. AC_ _om )
11 acndom 
 |-  ( A ~<_ _om -> ( U_ x e. A ( _om ^m B ) e. AC_ _om -> U_ x e. A ( _om ^m B ) e. AC_ A ) )
12 2 10 11 sylc 
 |-  ( ( A ~<_ _om /\ A. x e. A B ~<_ _om ) -> U_ x e. A ( _om ^m B ) e. AC_ A )
13 simpr 
 |-  ( ( A ~<_ _om /\ A. x e. A B ~<_ _om ) -> A. x e. A B ~<_ _om )
14 omex 
 |-  _om e. _V
15 xpdom1g 
 |-  ( ( _om e. _V /\ A ~<_ _om ) -> ( A X. _om ) ~<_ ( _om X. _om ) )
16 14 2 15 sylancr 
 |-  ( ( A ~<_ _om /\ A. x e. A B ~<_ _om ) -> ( A X. _om ) ~<_ ( _om X. _om ) )
17 xpomen 
 |-  ( _om X. _om ) ~~ _om
18 domentr 
 |-  ( ( ( A X. _om ) ~<_ ( _om X. _om ) /\ ( _om X. _om ) ~~ _om ) -> ( A X. _om ) ~<_ _om )
19 16 17 18 sylancl 
 |-  ( ( A ~<_ _om /\ A. x e. A B ~<_ _om ) -> ( A X. _om ) ~<_ _om )
20 ctex 
 |-  ( B ~<_ _om -> B e. _V )
21 20 ralimi 
 |-  ( A. x e. A B ~<_ _om -> A. x e. A B e. _V )
22 iunexg 
 |-  ( ( A e. _V /\ A. x e. A B e. _V ) -> U_ x e. A B e. _V )
23 3 21 22 syl2an 
 |-  ( ( A ~<_ _om /\ A. x e. A B ~<_ _om ) -> U_ x e. A B e. _V )
24 omelon 
 |-  _om e. On
25 onenon 
 |-  ( _om e. On -> _om e. dom card )
26 24 25 ax-mp 
 |-  _om e. dom card
27 numacn 
 |-  ( U_ x e. A B e. _V -> ( _om e. dom card -> _om e. AC_ U_ x e. A B ) )
28 23 26 27 mpisyl 
 |-  ( ( A ~<_ _om /\ A. x e. A B ~<_ _om ) -> _om e. AC_ U_ x e. A B )
29 acndom2 
 |-  ( ( A X. _om ) ~<_ _om -> ( _om e. AC_ U_ x e. A B -> ( A X. _om ) e. AC_ U_ x e. A B ) )
30 19 28 29 sylc 
 |-  ( ( A ~<_ _om /\ A. x e. A B ~<_ _om ) -> ( A X. _om ) e. AC_ U_ x e. A B )
31 1 12 13 30 iundomg 
 |-  ( ( A ~<_ _om /\ A. x e. A B ~<_ _om ) -> U_ x e. A B ~<_ ( A X. _om ) )
32 domtr 
 |-  ( ( U_ x e. A B ~<_ ( A X. _om ) /\ ( A X. _om ) ~<_ _om ) -> U_ x e. A B ~<_ _om )
33 31 19 32 syl2anc 
 |-  ( ( A ~<_ _om /\ A. x e. A B ~<_ _om ) -> U_ x e. A B ~<_ _om )