Theorem tpos0

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

	Ref	Expression
Assertion	tpos0	$$⊢tpos\varnothing =\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		rel0	$$⊢\mathrm{Rel}\varnothing$$
2		eqid	$$⊢\varnothing =\varnothing$$
3		fn0	$$⊢\varnothing Fn\varnothing \leftrightarrow \varnothing =\varnothing$$
4	2 3	mpbir	$$⊢\varnothing Fn\varnothing$$
5		tposfn2	$$⊢\mathrm{Rel}\varnothing \to \left(\varnothing Fn\varnothing \to tpos\varnothing Fn{\varnothing }^{-1}\right)$$
6	1 4 5	mp2	$$⊢tpos\varnothing Fn{\varnothing }^{-1}$$
7		cnv0	$$⊢{\varnothing }^{-1}=\varnothing$$
8	7	fneq2i	$$⊢tpos\varnothing Fn{\varnothing }^{-1}\leftrightarrow tpos\varnothing Fn\varnothing$$
9	6 8	mpbi	$$⊢tpos\varnothing Fn\varnothing$$
10		fn0	$$⊢tpos\varnothing Fn\varnothing \leftrightarrow tpos\varnothing =\varnothing$$
11	9 10	mpbi	$$⊢tpos\varnothing =\varnothing$$