Step |
Hyp |
Ref |
Expression |
1 |
|
rnmposs.1 |
|- F = ( x e. A , y e. B |-> C ) |
2 |
1
|
rnmpo |
|- ran F = { z | E. x e. A E. y e. B z = C } |
3 |
2
|
abeq2i |
|- ( z e. ran F <-> E. x e. A E. y e. B z = C ) |
4 |
|
2r19.29 |
|- ( ( A. x e. A A. y e. B C e. D /\ E. x e. A E. y e. B z = C ) -> E. x e. A E. y e. B ( C e. D /\ z = C ) ) |
5 |
|
eleq1 |
|- ( z = C -> ( z e. D <-> C e. D ) ) |
6 |
5
|
biimparc |
|- ( ( C e. D /\ z = C ) -> z e. D ) |
7 |
6
|
a1i |
|- ( ( x e. A /\ y e. B ) -> ( ( C e. D /\ z = C ) -> z e. D ) ) |
8 |
7
|
rexlimivv |
|- ( E. x e. A E. y e. B ( C e. D /\ z = C ) -> z e. D ) |
9 |
4 8
|
syl |
|- ( ( A. x e. A A. y e. B C e. D /\ E. x e. A E. y e. B z = C ) -> z e. D ) |
10 |
9
|
ex |
|- ( A. x e. A A. y e. B C e. D -> ( E. x e. A E. y e. B z = C -> z e. D ) ) |
11 |
3 10
|
syl5bi |
|- ( A. x e. A A. y e. B C e. D -> ( z e. ran F -> z e. D ) ) |
12 |
11
|
ssrdv |
|- ( A. x e. A A. y e. B C e. D -> ran F C_ D ) |