Metamath Proof Explorer

Theorem tposrescnv

Description: The transposition restricted to a converse is the transposition of the restricted class, with the empty set removed from the domain. Note that the right hand side is a more useful form of ` ( tpos ( F |`` R ) |`( _V \ { (/) } ) ) by df-tpos . (Contributed by Zhi Wang, 6-Oct-2025)

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

Proof

Step Hyp Ref Expression
1 df-tpos 
 |-  tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
2 1 reseq1i 
 |-  ( tpos F |` `' R ) = ( ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) |` `' R )
3 resco 
 |-  ( ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) ) |` `' R ) = ( F o. ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) |` `' R ) )
4 resmpt3 
 |-  ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) |` `' R ) = ( x e. ( ( `' dom F u. { (/) } ) i^i `' R ) |-> U. `' { x } )
5 cnvin 
 |-  `' ( R i^i dom F ) = ( `' R i^i `' dom F )
6 dmres 
 |-  dom ( F |` R ) = ( R i^i dom F )
7 6 cnveqi 
 |-  `' dom ( F |` R ) = `' ( R i^i dom F )
8 incom 
 |-  ( ( `' dom F u. { (/) } ) i^i `' R ) = ( `' R i^i ( `' dom F u. { (/) } ) )
9 indi 
 |-  ( `' R i^i ( `' dom F u. { (/) } ) ) = ( ( `' R i^i `' dom F ) u. ( `' R i^i { (/) } ) )
10 relcnv 
 |-  Rel `' R
11 0nelrel0 
 |-  ( Rel `' R -> -. (/) e. `' R )
12 10 11 ax-mp 
 |-  -. (/) e. `' R
13 disjsn 
 |-  ( ( `' R i^i { (/) } ) = (/) <-> -. (/) e. `' R )
14 12 13 mpbir 
 |-  ( `' R i^i { (/) } ) = (/)
15 14 uneq2i 
 |-  ( ( `' R i^i `' dom F ) u. ( `' R i^i { (/) } ) ) = ( ( `' R i^i `' dom F ) u. (/) )
16 un0 
 |-  ( ( `' R i^i `' dom F ) u. (/) ) = ( `' R i^i `' dom F )
17 15 16 eqtri 
 |-  ( ( `' R i^i `' dom F ) u. ( `' R i^i { (/) } ) ) = ( `' R i^i `' dom F )
18 8 9 17 3eqtri 
 |-  ( ( `' dom F u. { (/) } ) i^i `' R ) = ( `' R i^i `' dom F )
19 5 7 18 3eqtr4ri 
 |-  ( ( `' dom F u. { (/) } ) i^i `' R ) = `' dom ( F |` R )
20 19 mpteq1i 
 |-  ( x e. ( ( `' dom F u. { (/) } ) i^i `' R ) |-> U. `' { x } ) = ( x e. `' dom ( F |` R ) |-> U. `' { x } )
21 4 20 eqtri 
 |-  ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) |` `' R ) = ( x e. `' dom ( F |` R ) |-> U. `' { x } )
22 21 coeq2i 
 |-  ( F o. ( ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) |` `' R ) ) = ( F o. ( x e. `' dom ( F |` R ) |-> U. `' { x } ) )
23 2 3 22 3eqtri 
 |-  ( tpos F |` `' R ) = ( F o. ( x e. `' dom ( F |` R ) |-> U. `' { x } ) )