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 ◡ ∅ ) )
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 ∅ = ∅