Theorem tposexg

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

	Ref	Expression
Assertion	tposexg	|- ( F e. V -> tpos F e. _V )

Proof

Step	Hyp	Ref	Expression
1		tposssxp	|- tpos F C_ ( ( `' dom F u. { (/) } ) X. ran F )
2		dmexg	|- ( F e. V -> dom F e. _V )
3		cnvexg	|- ( dom F e. _V -> `' dom F e. _V )
4	2 3	syl	|- ( F e. V -> `' dom F e. _V )
5		p0ex	|- { (/) } e. _V
6		unexg	|- ( ( `' dom F e. _V /\ { (/) } e. _V ) -> ( `' dom F u. { (/) } ) e. _V )
7	4 5 6	sylancl	|- ( F e. V -> ( `' dom F u. { (/) } ) e. _V )
8		rnexg	|- ( F e. V -> ran F e. _V )
9	7 8	xpexd	|- ( F e. V -> ( ( `' dom F u. { (/) } ) X. ran F ) e. _V )
10		ssexg	|- ( ( tpos F C_ ( ( `' dom F u. { (/) } ) X. ran F ) /\ ( ( `' dom F u. { (/) } ) X. ran F ) e. _V ) -> tpos F e. _V )
11	1 9 10	sylancr	|- ( F e. V -> tpos F e. _V )