Definition df-tpos 8251

Description: Define the transposition of a function, which is a function 𝐺 = tpos 𝐹 satisfying 𝐺(𝑥, 𝑦) = 𝐹(𝑦, 𝑥). (Contributed by Mario Carneiro, 10-Sep-2015.)

Assertion

Ref	Expression
df-tpos	⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))

Distinct variable group:   𝑥,𝐹

Detailed syntax breakdown of Definition df-tpos

Step	Hyp	Ref	Expression
1		cF	. . 3 class 𝐹
2	1	ctpos 8250	. 2 class tpos 𝐹
3		vx	. . . 4 setvar 𝑥
4	1	cdm 5685	. . . . . 6 class dom 𝐹
5	4	ccnv 5684	. . . . 5 class ◡dom 𝐹
6		c0 4333	. . . . . 6 class ∅
7	6	csn 4626	. . . . 5 class {∅}
8	5, 7	cun 3949	. . . 4 class (◡dom 𝐹 ∪ {∅})
9	3	cv 1539	. . . . . . 7 class 𝑥
10	9	csn 4626	. . . . . 6 class {𝑥}
11	10	ccnv 5684	. . . . 5 class ◡{𝑥}
12	11	cuni 4907	. . . 4 class ∪ ◡{𝑥}
13	3, 8, 12	cmpt 5225	. . 3 class (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})
14	1, 13	ccom 5689	. 2 class (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))
15	2, 14	wceq 1540	1 wff tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))

This definition is referenced by:  tposss  8252  tposssxp  8255  brtpos2  8257  tposfun  8267  dftpos2  8268  dftpos4  8270  dftpos5  48774  dmtposss  48776  tposrescnv  48779