Theorem tposexg

Description: The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015)

	Ref	Expression
Assertion	tposexg	$$⊢F\in V\to tposF\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		tposssxp	$$⊢tposF\subseteq \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)\times \mathrm{ran}F$$
2		dmexg	$$⊢F\in V\to \mathrm{dom}F\in \mathrm{V}$$
3		cnvexg	$$⊢\mathrm{dom}F\in \mathrm{V}\to {\mathrm{dom}F}^{-1}\in \mathrm{V}$$
4	2 3	syl	$$⊢F\in V\to {\mathrm{dom}F}^{-1}\in \mathrm{V}$$
5		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
6		unexg	$$⊢\left({\mathrm{dom}F}^{-1}\in \mathrm{V}\wedge \left\{\varnothing \right\}\in \mathrm{V}\right)\to {\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\in \mathrm{V}$$
7	4 5 6	sylancl	$$⊢F\in V\to {\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\in \mathrm{V}$$
8		rnexg	$$⊢F\in V\to \mathrm{ran}F\in \mathrm{V}$$
9	7 8	xpexd	$$⊢F\in V\to \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)\times \mathrm{ran}F\in \mathrm{V}$$
10		ssexg	$$⊢\left(tposF\subseteq \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)\times \mathrm{ran}F\wedge \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)\times \mathrm{ran}F\in \mathrm{V}\right)\to tposF\in \mathrm{V}$$
11	1 9 10	sylancr	$$⊢F\in V\to tposF\in \mathrm{V}$$