Step |
Hyp |
Ref |
Expression |
1 |
|
cnv0 |
|- `' (/) = (/) |
2 |
|
cnvco |
|- `' ( (/) o. A ) = ( `' A o. `' (/) ) |
3 |
1
|
coeq2i |
|- ( `' A o. `' (/) ) = ( `' A o. (/) ) |
4 |
|
co02 |
|- ( `' A o. (/) ) = (/) |
5 |
2 3 4
|
3eqtri |
|- `' ( (/) o. A ) = (/) |
6 |
1 5
|
eqtr4i |
|- `' (/) = `' ( (/) o. A ) |
7 |
6
|
cnveqi |
|- `' `' (/) = `' `' ( (/) o. A ) |
8 |
|
rel0 |
|- Rel (/) |
9 |
|
dfrel2 |
|- ( Rel (/) <-> `' `' (/) = (/) ) |
10 |
8 9
|
mpbi |
|- `' `' (/) = (/) |
11 |
|
relco |
|- Rel ( (/) o. A ) |
12 |
|
dfrel2 |
|- ( Rel ( (/) o. A ) <-> `' `' ( (/) o. A ) = ( (/) o. A ) ) |
13 |
11 12
|
mpbi |
|- `' `' ( (/) o. A ) = ( (/) o. A ) |
14 |
7 10 13
|
3eqtr3ri |
|- ( (/) o. A ) = (/) |