Step |
Hyp |
Ref |
Expression |
1 |
|
frel |
|- ( F : A --> B -> Rel F ) |
2 |
|
relssdmrn |
|- ( Rel F -> F C_ ( dom F X. ran F ) ) |
3 |
1 2
|
syl |
|- ( F : A --> B -> F C_ ( dom F X. ran F ) ) |
4 |
|
fdm |
|- ( F : A --> B -> dom F = A ) |
5 |
|
eqimss |
|- ( dom F = A -> dom F C_ A ) |
6 |
4 5
|
syl |
|- ( F : A --> B -> dom F C_ A ) |
7 |
|
frn |
|- ( F : A --> B -> ran F C_ B ) |
8 |
|
xpss12 |
|- ( ( dom F C_ A /\ ran F C_ B ) -> ( dom F X. ran F ) C_ ( A X. B ) ) |
9 |
6 7 8
|
syl2anc |
|- ( F : A --> B -> ( dom F X. ran F ) C_ ( A X. B ) ) |
10 |
3 9
|
sstrd |
|- ( F : A --> B -> F C_ ( A X. B ) ) |