| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fvconstr.1 |
|- ( ph -> F = ( R X. { Y } ) ) |
| 2 |
|
fvconstr2.2 |
|- ( ph -> X e. ( A F B ) ) |
| 3 |
2
|
ne0d |
|- ( ph -> ( A F B ) =/= (/) ) |
| 4 |
1
|
oveqd |
|- ( ph -> ( A F B ) = ( A ( R X. { Y } ) B ) ) |
| 5 |
|
df-ov |
|- ( A ( R X. { Y } ) B ) = ( ( R X. { Y } ) ` <. A , B >. ) |
| 6 |
4 5
|
eqtrdi |
|- ( ph -> ( A F B ) = ( ( R X. { Y } ) ` <. A , B >. ) ) |
| 7 |
6
|
neeq1d |
|- ( ph -> ( ( A F B ) =/= (/) <-> ( ( R X. { Y } ) ` <. A , B >. ) =/= (/) ) ) |
| 8 |
|
dmxpss |
|- dom ( R X. { Y } ) C_ R |
| 9 |
|
ndmfv |
|- ( -. <. A , B >. e. dom ( R X. { Y } ) -> ( ( R X. { Y } ) ` <. A , B >. ) = (/) ) |
| 10 |
9
|
necon1ai |
|- ( ( ( R X. { Y } ) ` <. A , B >. ) =/= (/) -> <. A , B >. e. dom ( R X. { Y } ) ) |
| 11 |
8 10
|
sselid |
|- ( ( ( R X. { Y } ) ` <. A , B >. ) =/= (/) -> <. A , B >. e. R ) |
| 12 |
7 11
|
biimtrdi |
|- ( ph -> ( ( A F B ) =/= (/) -> <. A , B >. e. R ) ) |
| 13 |
3 12
|
mpd |
|- ( ph -> <. A , B >. e. R ) |
| 14 |
|
df-br |
|- ( A R B <-> <. A , B >. e. R ) |
| 15 |
13 14
|
sylibr |
|- ( ph -> A R B ) |