Metamath Proof Explorer

Theorem tposss

Description: Subset theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion tposss 
|- ( F C_ G -> tpos F C_ tpos G )

Proof

Step Hyp Ref Expression
1 coss1 
 |-  ( F C_ G -> ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) C_ ( G o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) )
2 dmss 
 |-  ( F C_ G -> dom F C_ dom G )
3 cnvss 
 |-  ( dom F C_ dom G -> `' dom F C_ `' dom G )
4 unss1 
 |-  ( `' dom F C_ `' dom G -> ( `' dom F u. { (/) } ) C_ ( `' dom G u. { (/) } ) )
5 resmpt 
 |-  ( ( `' dom F u. { (/) } ) C_ ( `' dom G u. { (/) } ) -> ( ( x e. ( `' dom G u. { (/) } ) |-> U. `' { x } ) |` ( `' dom F u. { (/) } ) ) = ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
6 2 3 4 5 4syl 
 |-  ( F C_ G -> ( ( x e. ( `' dom G u. { (/) } ) |-> U. `' { x } ) |` ( `' dom F u. { (/) } ) ) = ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
7 resss 
 |-  ( ( x e. ( `' dom G u. { (/) } ) |-> U. `' { x } ) |` ( `' dom F u. { (/) } ) ) C_ ( x e. ( `' dom G u. { (/) } ) |-> U. `' { x } )
8 6 7 eqsstrrdi 
 |-  ( F C_ G -> ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) C_ ( x e. ( `' dom G u. { (/) } ) |-> U. `' { x } ) )
9 coss2 
 |-  ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) C_ ( x e. ( `' dom G u. { (/) } ) |-> U. `' { x } ) -> ( G o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) C_ ( G o. ( x e. ( `' dom G u. { (/) } ) |-> U. `' { x } ) ) )
10 8 9 syl 
 |-  ( F C_ G -> ( G o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) C_ ( G o. ( x e. ( `' dom G u. { (/) } ) |-> U. `' { x } ) ) )
11 1 10 sstrd 
 |-  ( F C_ G -> ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) C_ ( G o. ( x e. ( `' dom G u. { (/) } ) |-> U. `' { x } ) ) )
12 df-tpos 
 |-  tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
13 df-tpos 
 |-  tpos G = ( G o. ( x e. ( `' dom G u. { (/) } ) |-> U. `' { x } ) )
14 11 12 13 3sstr4g 
 |-  ( F C_ G -> tpos F C_ tpos G )