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

Metamath Proof Explorer

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