Description: Transposition of the empty set. (Contributed by NM, 10-Sep-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | tpos0 | |- tpos (/) = (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rel0 | |- Rel (/) |
|
| 2 | eqid | |- (/) = (/) |
|
| 3 | fn0 | |- ( (/) Fn (/) <-> (/) = (/) ) |
|
| 4 | 2 3 | mpbir | |- (/) Fn (/) |
| 5 | tposfn2 | |- ( Rel (/) -> ( (/) Fn (/) -> tpos (/) Fn `' (/) ) ) |
|
| 6 | 1 4 5 | mp2 | |- tpos (/) Fn `' (/) |
| 7 | cnv0 | |- `' (/) = (/) |
|
| 8 | 7 | fneq2i | |- ( tpos (/) Fn `' (/) <-> tpos (/) Fn (/) ) |
| 9 | 6 8 | mpbi | |- tpos (/) Fn (/) |
| 10 | fn0 | |- ( tpos (/) Fn (/) <-> tpos (/) = (/) ) |
|
| 11 | 9 10 | mpbi | |- tpos (/) = (/) |