Step |
Hyp |
Ref |
Expression |
1 |
|
dfdisjs2 |
|- Disjs = { r e. Rels | ,~ `' r C_ _I } |
2 |
|
cosscnvssid5 |
|- ( ( ,~ `' r C_ _I /\ Rel r ) <-> ( A. u e. dom r A. v e. dom r ( u = v \/ ( [ u ] r i^i [ v ] r ) = (/) ) /\ Rel r ) ) |
3 |
|
elrelsrelim |
|- ( r e. Rels -> Rel r ) |
4 |
3
|
biantrud |
|- ( r e. Rels -> ( ,~ `' r C_ _I <-> ( ,~ `' r C_ _I /\ Rel r ) ) ) |
5 |
3
|
biantrud |
|- ( r e. Rels -> ( A. u e. dom r A. v e. dom r ( u = v \/ ( [ u ] r i^i [ v ] r ) = (/) ) <-> ( A. u e. dom r A. v e. dom r ( u = v \/ ( [ u ] r i^i [ v ] r ) = (/) ) /\ Rel r ) ) ) |
6 |
4 5
|
bibi12d |
|- ( r e. Rels -> ( ( ,~ `' r C_ _I <-> A. u e. dom r A. v e. dom r ( u = v \/ ( [ u ] r i^i [ v ] r ) = (/) ) ) <-> ( ( ,~ `' r C_ _I /\ Rel r ) <-> ( A. u e. dom r A. v e. dom r ( u = v \/ ( [ u ] r i^i [ v ] r ) = (/) ) /\ Rel r ) ) ) ) |
7 |
2 6
|
mpbiri |
|- ( r e. Rels -> ( ,~ `' r C_ _I <-> A. u e. dom r A. v e. dom r ( u = v \/ ( [ u ] r i^i [ v ] r ) = (/) ) ) ) |
8 |
1 7
|
rabimbieq |
|- Disjs = { r e. Rels | A. u e. dom r A. v e. dom r ( u = v \/ ( [ u ] r i^i [ v ] r ) = (/) ) } |