Definition df-cnv2 35777

Description: Define a function that returns the second converse of a set. The second converse of a set takes all ordered triples in the set and rotates them so the last argument becomes the first argument. Based on Definition 14.1(1) of [TakeutiZaring] p. 143. (Contributed by BTernaryTau, 2-Sep-2026.)

Assertion

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

Distinct variable group:   𝑥,𝑤,𝑦,𝑧

Detailed syntax breakdown of Definition df-cnv2

Step	Hyp	Ref	Expression
1		ccnv2 35766	. 2 class Cnv2
2		vw	. . 3 setvar 𝑤
3		cvv 3450	. . 3 class V
4		vz	. . . . . . . 8 setvar 𝑧
5	4	cv 1569	. . . . . . 7 class 𝑧
6		vx	. . . . . . . 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, 6, 9, 4	coprab 7409	. . 3 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ⟨⟨𝑧, 𝑥⟩, 𝑦⟩ ∈ 𝑤}
15	2, 3, 14	cmpt 5185	. 2 class (𝑤 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ⟨⟨𝑧, 𝑥⟩, 𝑦⟩ ∈ 𝑤})
16	1, 15	wceq 1570	1 wff Cnv2 = (𝑤 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ⟨⟨𝑧, 𝑥⟩, 𝑦⟩ ∈ 𝑤})

This definition is used by: (None)