Definition df-cnv3 35778

Description: Define a function that returns the third converse of a set. The third converse of a set takes all ordered triples in the set and swaps the second and third arguments. Based on Definition 14.1(2) of [TakeutiZaring] p. 143. (Contributed by BTernaryTau, 2-Sep-2026.)

Assertion

Ref	Expression
df-cnv3	⊢ Cnv3 = (𝑤 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∈ 𝑤})

Distinct variable group:   𝑥,𝑤,𝑦,𝑧

Detailed syntax breakdown of Definition df-cnv3

Step	Hyp	Ref	Expression
1		ccnv3 35767	. 2 class Cnv3
2		vw	. . 3 setvar 𝑤
3		cvv 3450	. . 3 class V
4		vx	. . . . . . . 8 setvar 𝑥
5	4	cv 1569	. . . . . . 7 class 𝑥
6		vz	. . . . . . . 8 setvar 𝑧
7	6	cv 1569	. . . . . . 7 class 𝑧
8	5, 7	cop 4589	. . . . . 6 class ⟨𝑥, 𝑧⟩
9		vy	. . . . . . 7 setvar 𝑦
10	9	cv 1569	. . . . . 6 class 𝑦
11	8, 10	cop 4589	. . . . 5 class ⟨⟨𝑥, 𝑧⟩, 𝑦⟩
12	2	cv 1569	. . . . 5 class 𝑤
13	11, 12	wcel 2145	. . . 4 wff ⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∈ 𝑤
14	13, 4, 9, 6	coprab 7409	. . 3 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∈ 𝑤}
15	2, 3, 14	cmpt 5185	. 2 class (𝑤 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∈ 𝑤})
16	1, 15	wceq 1570	1 wff Cnv3 = (𝑤 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∈ 𝑤})

This definition is used by: (None)