| Step |
Hyp |
Ref |
Expression |
| 1 |
|
oprssdm.1 |
|- -. (/) e. S |
| 2 |
|
oprssdm.2 |
|- ( ( x e. S /\ y e. S ) -> ( x F y ) e. S ) |
| 3 |
|
relxp |
|- Rel ( S X. S ) |
| 4 |
|
opelxp |
|- ( <. x , y >. e. ( S X. S ) <-> ( x e. S /\ y e. S ) ) |
| 5 |
|
df-ov |
|- ( x F y ) = ( F ` <. x , y >. ) |
| 6 |
5 2
|
eqeltrrid |
|- ( ( x e. S /\ y e. S ) -> ( F ` <. x , y >. ) e. S ) |
| 7 |
|
ndmfv |
|- ( -. <. x , y >. e. dom F -> ( F ` <. x , y >. ) = (/) ) |
| 8 |
7
|
eleq1d |
|- ( -. <. x , y >. e. dom F -> ( ( F ` <. x , y >. ) e. S <-> (/) e. S ) ) |
| 9 |
1 8
|
mtbiri |
|- ( -. <. x , y >. e. dom F -> -. ( F ` <. x , y >. ) e. S ) |
| 10 |
9
|
con4i |
|- ( ( F ` <. x , y >. ) e. S -> <. x , y >. e. dom F ) |
| 11 |
6 10
|
syl |
|- ( ( x e. S /\ y e. S ) -> <. x , y >. e. dom F ) |
| 12 |
4 11
|
sylbi |
|- ( <. x , y >. e. ( S X. S ) -> <. x , y >. e. dom F ) |
| 13 |
3 12
|
relssi |
|- ( S X. S ) C_ dom F |