Metamath Proof Explorer

Theorem tposres3

Description: The transposition restricted to a set. (Contributed by Zhi Wang, 6-Oct-2025)

Ref Expression
Hypothesis tposres2.1 
|- ( ph -> -. (/) e. ( dom F i^i R ) )
Assertion tposres3 
|- ( ph -> ( tpos F |` R ) = tpos ( F |` `' R ) )

Proof

Step Hyp Ref Expression
1 tposres2.1 
 |-  ( ph -> -. (/) e. ( dom F i^i R ) )
2 1 tposres2 
 |-  ( ph -> ( tpos F |` R ) = ( tpos F |` `' `' R ) )
3 relcnv 
 |-  Rel `' dom ( F |` `' R )
4 cnvf1o 
 |-  ( Rel `' dom ( F |` `' R ) -> ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) : `' dom ( F |` `' R ) -1-1-onto-> `' `' dom ( F |` `' R ) )
5 3 4 ax-mp 
 |-  ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) : `' dom ( F |` `' R ) -1-1-onto-> `' `' dom ( F |` `' R )
6 f1ofo 
 |-  ( ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) : `' dom ( F |` `' R ) -1-1-onto-> `' `' dom ( F |` `' R ) -> ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) : `' dom ( F |` `' R ) -onto-> `' `' dom ( F |` `' R ) )
7 5 6 ax-mp 
 |-  ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) : `' dom ( F |` `' R ) -onto-> `' `' dom ( F |` `' R )
8 forn 
 |-  ( ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) : `' dom ( F |` `' R ) -onto-> `' `' dom ( F |` `' R ) -> ran ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) = `' `' dom ( F |` `' R ) )
9 7 8 ax-mp 
 |-  ran ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) = `' `' dom ( F |` `' R )
10 cnvcnvss 
 |-  `' `' dom ( F |` `' R ) C_ dom ( F |` `' R )
11 resdmss 
 |-  dom ( F |` `' R ) C_ `' R
12 10 11 sstri 
 |-  `' `' dom ( F |` `' R ) C_ `' R
13 9 12 eqsstri 
 |-  ran ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) C_ `' R
14 cores 
 |-  ( ran ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) C_ `' R -> ( ( F |` `' R ) o. ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) ) = ( F o. ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) ) )
15 13 14 ax-mp 
 |-  ( ( F |` `' R ) o. ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) ) = ( F o. ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) )
16 dftpos6 
 |-  tpos ( F |` `' R ) = ( ( ( F |` `' R ) o. ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) ) u. ( { (/) } X. ( ( F |` `' R ) " { (/) } ) ) )
17 ressn 
 |-  ( ( F |` `' R ) |` { (/) } ) = ( { (/) } X. ( ( F |` `' R ) " { (/) } ) )
18 resres 
 |-  ( ( F |` `' R ) |` { (/) } ) = ( F |` ( `' R i^i { (/) } ) )
19 relcnv 
 |-  Rel `' R
20 0nelrel0 
 |-  ( Rel `' R -> -. (/) e. `' R )
21 19 20 ax-mp 
 |-  -. (/) e. `' R
22 disjsn 
 |-  ( ( `' R i^i { (/) } ) = (/) <-> -. (/) e. `' R )
23 21 22 mpbir 
 |-  ( `' R i^i { (/) } ) = (/)
24 23 reseq2i 
 |-  ( F |` ( `' R i^i { (/) } ) ) = ( F |` (/) )
25 res0 
 |-  ( F |` (/) ) = (/)
26 18 24 25 3eqtri 
 |-  ( ( F |` `' R ) |` { (/) } ) = (/)
27 17 26 eqtr3i 
 |-  ( { (/) } X. ( ( F |` `' R ) " { (/) } ) ) = (/)
28 27 uneq2i 
 |-  ( ( ( F |` `' R ) o. ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) ) u. ( { (/) } X. ( ( F |` `' R ) " { (/) } ) ) ) = ( ( ( F |` `' R ) o. ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) ) u. (/) )
29 un0 
 |-  ( ( ( F |` `' R ) o. ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) ) u. (/) ) = ( ( F |` `' R ) o. ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) )
30 16 28 29 3eqtri 
 |-  tpos ( F |` `' R ) = ( ( F |` `' R ) o. ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) )
31 tposrescnv 
 |-  ( tpos F |` `' `' R ) = ( F o. ( x e. `' dom ( F |` `' R ) |-> U. `' { x } ) )
32 15 30 31 3eqtr4ri 
 |-  ( tpos F |` `' `' R ) = tpos ( F |` `' R )
33 2 32 eqtrdi 
 |-  ( ph -> ( tpos F |` R ) = tpos ( F |` `' R ) )