This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tpos0

Description: Transposition of the empty set. (Contributed by NM, 10-Sep-2015)

Ref Expression
Assertion tpos0 ⊢ tpos ∅ = ∅

Proof

Step Hyp Ref Expression
1 rel0 ⊢ Rel ⁡ ∅
2 eqid ⊢ ∅ = ∅
3 fn0 ⊢ ∅ Fn ∅ ↔ ∅ = ∅
4 2 3 mpbir ⊢ ∅ Fn ∅
5 tposfn2 ⊢ Rel ⁡ ∅ → ∅ Fn ∅ → tpos ∅ Fn ∅ -1
6 1 4 5 mp2 ⊢ tpos ∅ Fn ∅ -1
7 cnv0 ⊢ ∅ -1 = ∅
8 7 fneq2i ⊢ tpos ∅ Fn ∅ -1 ↔ tpos ∅ Fn ∅
9 6 8 mpbi ⊢ tpos ∅ Fn ∅
10 fn0 ⊢ tpos ∅ Fn ∅ ↔ tpos ∅ = ∅
11 9 10 mpbi ⊢ tpos ∅ = ∅