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