Theorem tposssxp

Description: The transposition is a subset of a Cartesian product. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Assertion	tposssxp	|- tpos F C_ ( ( `' dom F u. { (/) } ) X. ran F )

Proof

Step	Hyp	Ref	Expression
1		df-tpos	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
2		cossxp	|- ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) C_ ( dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) X. ran F )
3	1 2	eqsstri	|- tpos F C_ ( dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) X. ran F )
4		eqid	|- ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) = ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } )
5	4	dmmptss	|- dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) C_ ( `' dom F u. { (/) } )
6		xpss1	|- ( dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) C_ ( `' dom F u. { (/) } ) -> ( dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) X. ran F ) C_ ( ( `' dom F u. { (/) } ) X. ran F ) )
7	5 6	ax-mp	|- ( dom ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) X. ran F ) C_ ( ( `' dom F u. { (/) } ) X. ran F )
8	3 7	sstri	|- tpos F C_ ( ( `' dom F u. { (/) } ) X. ran F )