This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )