Metamath Proof Explorer

Theorem dftpos2

Description: Alternate definition of tpos when F has relational domain. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion dftpos2 
|- ( Rel dom F -> tpos F = ( F o. ( x e. `' dom F |-> U. `' { x } ) ) )

Proof

Step Hyp Ref Expression
1 dmtpos 
 |-  ( Rel dom F -> dom tpos F = `' dom F )
2 1 reseq2d 
 |-  ( Rel dom F -> ( tpos F |` dom tpos F ) = ( tpos F |` `' dom F ) )
3 reltpos 
 |-  Rel tpos F
4 resdm 
 |-  ( Rel tpos F -> ( tpos F |` dom tpos F ) = tpos F )
5 3 4 ax-mp 
 |-  ( tpos F |` dom tpos F ) = tpos F
6 df-tpos 
 |-  tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
7 6 reseq1i 
 |-  ( tpos F |` `' dom F ) = ( ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) |` `' dom F )
8 resco 
 |-  ( ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) |` `' dom F ) = ( F o. ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) |` `' dom F ) )
9 ssun1 
 |-  `' dom F C_ ( `' dom F u. { (/) } )
10 resmpt 
 |-  ( `' dom F C_ ( `' dom F u. { (/) } ) -> ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) |` `' dom F ) = ( x e. `' dom F |-> U. `' { x } ) )
11 9 10 ax-mp 
 |-  ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) |` `' dom F ) = ( x e. `' dom F |-> U. `' { x } )
12 11 coeq2i 
 |-  ( F o. ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) |` `' dom F ) ) = ( F o. ( x e. `' dom F |-> U. `' { x } ) )
13 7 8 12 3eqtri 
 |-  ( tpos F |` `' dom F ) = ( F o. ( x e. `' dom F |-> U. `' { x } ) )
14 2 5 13 3eqtr3g 
 |-  ( Rel dom F -> tpos F = ( F o. ( x e. `' dom F |-> U. `' { x } ) ) )