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 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cF ⊢ 𝐹
1 0 ctpos ⊢ tpos 𝐹
2 vx ⊢ 𝑥
3 0 cdm ⊢ dom 𝐹
4 3 ccnv ⊢ ◡ dom 𝐹
5 c0 ⊢ ∅
6 5 csn ⊢ { ∅ }
7 4 6 cun ⊢ ( ◡ dom 𝐹 ∪ { ∅ } )
8 2 cv ⊢ 𝑥
9 8 csn ⊢ { 𝑥 }
10 9 ccnv ⊢ ◡ { 𝑥 }
11 10 cuni ⊢ ∪ ◡ { 𝑥 }
12 2 7 11 cmpt ⊢ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } )
13 0 12 ccom ⊢ ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
14 1 13 wceq ⊢ tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )