Step |
Hyp |
Ref |
Expression |
1 |
|
dom2d.1 |
|- ( ph -> ( x e. A -> C e. B ) ) |
2 |
|
dom2d.2 |
|- ( ph -> ( ( x e. A /\ y e. A ) -> ( C = D <-> x = y ) ) ) |
3 |
|
dom3d.3 |
|- ( ph -> A e. V ) |
4 |
|
dom3d.4 |
|- ( ph -> B e. W ) |
5 |
1 2
|
dom2lem |
|- ( ph -> ( x e. A |-> C ) : A -1-1-> B ) |
6 |
|
f1f |
|- ( ( x e. A |-> C ) : A -1-1-> B -> ( x e. A |-> C ) : A --> B ) |
7 |
5 6
|
syl |
|- ( ph -> ( x e. A |-> C ) : A --> B ) |
8 |
|
fex2 |
|- ( ( ( x e. A |-> C ) : A --> B /\ A e. V /\ B e. W ) -> ( x e. A |-> C ) e. _V ) |
9 |
7 3 4 8
|
syl3anc |
|- ( ph -> ( x e. A |-> C ) e. _V ) |
10 |
|
f1eq1 |
|- ( z = ( x e. A |-> C ) -> ( z : A -1-1-> B <-> ( x e. A |-> C ) : A -1-1-> B ) ) |
11 |
9 5 10
|
spcedv |
|- ( ph -> E. z z : A -1-1-> B ) |
12 |
|
brdomg |
|- ( B e. W -> ( A ~<_ B <-> E. z z : A -1-1-> B ) ) |
13 |
4 12
|
syl |
|- ( ph -> ( A ~<_ B <-> E. z z : A -1-1-> B ) ) |
14 |
11 13
|
mpbird |
|- ( ph -> A ~<_ B ) |