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

Metamath Proof Explorer

Theorem iundom

Description: An upper bound for the cardinality of an indexed union. C depends on x and should be thought of as C ( x ) . (Contributed by NM, 26-Mar-2006)

Ref Expression
Assertion iundom 
|- ( ( A e. V /\ A. x e. A C ~<_ B ) -> U_ x e. A C ~<_ ( A X. B ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U_ x e. A ( { x } X. C ) = U_ x e. A ( { x } X. C )
2 simpl 
 |-  ( ( A e. V /\ A. x e. A C ~<_ B ) -> A e. V )
3 ovex 
 |-  ( B ^m C ) e. _V
4 3 rgenw 
 |-  A. x e. A ( B ^m C ) e. _V
5 iunexg 
 |-  ( ( A e. V /\ A. x e. A ( B ^m C ) e. _V ) -> U_ x e. A ( B ^m C ) e. _V )
6 2 4 5 sylancl 
 |-  ( ( A e. V /\ A. x e. A C ~<_ B ) -> U_ x e. A ( B ^m C ) e. _V )
7 numth3 
 |-  ( U_ x e. A ( B ^m C ) e. _V -> U_ x e. A ( B ^m C ) e. dom card )
8 6 7 syl 
 |-  ( ( A e. V /\ A. x e. A C ~<_ B ) -> U_ x e. A ( B ^m C ) e. dom card )
9 numacn 
 |-  ( A e. V -> ( U_ x e. A ( B ^m C ) e. dom card -> U_ x e. A ( B ^m C ) e. AC_ A ) )
10 2 8 9 sylc 
 |-  ( ( A e. V /\ A. x e. A C ~<_ B ) -> U_ x e. A ( B ^m C ) e. AC_ A )
11 simpr 
 |-  ( ( A e. V /\ A. x e. A C ~<_ B ) -> A. x e. A C ~<_ B )
12 reldom 
 |-  Rel ~<_
13 12 brrelex1i 
 |-  ( C ~<_ B -> C e. _V )
14 13 ralimi 
 |-  ( A. x e. A C ~<_ B -> A. x e. A C e. _V )
15 iunexg 
 |-  ( ( A e. V /\ A. x e. A C e. _V ) -> U_ x e. A C e. _V )
16 14 15 sylan2 
 |-  ( ( A e. V /\ A. x e. A C ~<_ B ) -> U_ x e. A C e. _V )
17 1 10 11 iundom2g 
 |-  ( ( A e. V /\ A. x e. A C ~<_ B ) -> U_ x e. A ( { x } X. C ) ~<_ ( A X. B ) )
18 12 brrelex2i 
 |-  ( U_ x e. A ( { x } X. C ) ~<_ ( A X. B ) -> ( A X. B ) e. _V )
19 numth3 
 |-  ( ( A X. B ) e. _V -> ( A X. B ) e. dom card )
20 17 18 19 3syl 
 |-  ( ( A e. V /\ A. x e. A C ~<_ B ) -> ( A X. B ) e. dom card )
21 numacn 
 |-  ( U_ x e. A C e. _V -> ( ( A X. B ) e. dom card -> ( A X. B ) e. AC_ U_ x e. A C ) )
22 16 20 21 sylc 
 |-  ( ( A e. V /\ A. x e. A C ~<_ B ) -> ( A X. B ) e. AC_ U_ x e. A C )
23 1 10 11 22 iundomg 
 |-  ( ( A e. V /\ A. x e. A C ~<_ B ) -> U_ x e. A C ~<_ ( A X. B ) )