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 ) )