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