| Step |
Hyp |
Ref |
Expression |
| 1 |
|
relres |
|- Rel ( R |` A ) |
| 2 |
|
dfdisjALTV4 |
|- ( Disj ( R |` A ) <-> ( A. x E* u u ( R |` A ) x /\ Rel ( R |` A ) ) ) |
| 3 |
1 2
|
mpbiran2 |
|- ( Disj ( R |` A ) <-> A. x E* u u ( R |` A ) x ) |
| 4 |
|
brres |
|- ( x e. _V -> ( u ( R |` A ) x <-> ( u e. A /\ u R x ) ) ) |
| 5 |
4
|
elv |
|- ( u ( R |` A ) x <-> ( u e. A /\ u R x ) ) |
| 6 |
5
|
mobii |
|- ( E* u u ( R |` A ) x <-> E* u ( u e. A /\ u R x ) ) |
| 7 |
|
df-rmo |
|- ( E* u e. A u R x <-> E* u ( u e. A /\ u R x ) ) |
| 8 |
6 7
|
bitr4i |
|- ( E* u u ( R |` A ) x <-> E* u e. A u R x ) |
| 9 |
8
|
albii |
|- ( A. x E* u u ( R |` A ) x <-> A. x E* u e. A u R x ) |
| 10 |
3 9
|
bitri |
|- ( Disj ( R |` A ) <-> A. x E* u e. A u R x ) |
| 11 |
|
id |
|- ( u = v -> u = v ) |
| 12 |
11
|
inecmo |
|- ( Rel R -> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) <-> A. x E* u e. A u R x ) ) |
| 13 |
10 12
|
bitr4id |
|- ( Rel R -> ( Disj ( R |` A ) <-> A. u e. A A. v e. A ( u = v \/ ( [ u ] R i^i [ v ] R ) = (/) ) ) ) |