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 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )