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

Metamath Proof Explorer

Definition df-tpos

Description: Define the transposition of a function, which is a function G = tpos F satisfying G ( x , y ) = F ( y , x ) . (Contributed by Mario Carneiro, 10-Sep-2015)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cF 
 |-  F
1 0 ctpos 
 |-  tpos F
2 vx 
 |-  x
3 0 cdm 
 |-  dom F
4 3 ccnv 
 |-  `' dom F
5 c0 
 |-  (/)
6 5 csn 
 |-  { (/) }
7 4 6 cun 
 |-  ( `' dom F u. { (/) } )
8 2 cv 
 |-  x
9 8 csn 
 |-  { x }
10 9 ccnv 
 |-  `' { x }
11 10 cuni 
 |-  U. `' { x }
12 2 7 11 cmpt 
 |-  ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } )
13 0 12 ccom 
 |-  ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
14 1 13 wceq 
 |-  tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )