Theorem iundomg

Description: An upper bound for the cardinality of an indexed union, with explicit choice principles. B depends on x and should be thought of as B ( x ) . (Contributed by Mario Carneiro, 1-Sep-2015)

	Ref	Expression
Hypotheses	iunfo.1	|- T = U_ x e. A ( { x } X. B )
	iundomg.2	|- ( ph -> U_ x e. A ( C ^m B ) e. AC_ A )
	iundomg.3	|- ( ph -> A. x e. A B ~<_ C )
	iundomg.4	|- ( ph -> ( A X. C ) e. AC_ U_ x e. A B )
Assertion	iundomg	|- ( ph -> U_ x e. A B ~<_ ( A X. C ) )

Proof

Step	Hyp	Ref	Expression
1		iunfo.1	|- T = U_ x e. A ( { x } X. B )
2		iundomg.2	|- ( ph -> U_ x e. A ( C ^m B ) e. AC_ A )
3		iundomg.3	|- ( ph -> A. x e. A B ~<_ C )
4		iundomg.4	|- ( ph -> ( A X. C ) e. AC_ U_ x e. A B )
5	1 2 3	iundom2g	|- ( ph -> T ~<_ ( A X. C ) )
6		acndom2	|- ( T ~<_ ( A X. C ) -> ( ( A X. C ) e. AC_ U_ x e. A B -> T e. AC_ U_ x e. A B ) )
7	5 4 6	sylc	|- ( ph -> T e. AC_ U_ x e. A B )
8	1	iunfo	|- ( 2nd |` T ) : T -onto-> U_ x e. A B
9		fodomacn	|- ( T e. AC_ U_ x e. A B -> ( ( 2nd |` T ) : T -onto-> U_ x e. A B -> U_ x e. A B ~<_ T ) )
10	7 8 9	mpisyl	|- ( ph -> U_ x e. A B ~<_ T )
11		domtr	|- ( ( U_ x e. A B ~<_ T /\ T ~<_ ( A X. C ) ) -> U_ x e. A B ~<_ ( A X. C ) )
12	10 5 11	syl2anc	|- ( ph -> U_ x e. A B ~<_ ( A X. C ) )