Definition df-cnv3

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnv3	⊢ Cnv3
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		vy	⊢ 𝑦
5		vz	⊢ 𝑧
6	3	cv	⊢ 𝑥
7	5	cv	⊢ 𝑧
8	6 7	cop	⊢ ⟨ 𝑥 , 𝑧 ⟩
9	4	cv	⊢ 𝑦
10	8 9	cop	⊢ ⟨ ⟨ 𝑥 , 𝑧 ⟩ , 𝑦 ⟩
11	1	cv	⊢ 𝑤
12	10 11	wcel	⊢ ⟨ ⟨ 𝑥 , 𝑧 ⟩ , 𝑦 ⟩ ∈ 𝑤
13	12 3 4 5	coprab	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ⟨ ⟨ 𝑥 , 𝑧 ⟩ , 𝑦 ⟩ ∈ 𝑤 }
14	1 2 13	cmpt	⊢ ( 𝑤 ∈ V ↦ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ⟨ ⟨ 𝑥 , 𝑧 ⟩ , 𝑦 ⟩ ∈ 𝑤 } )
15	0 14	wceq	⊢ Cnv3 = ( 𝑤 ∈ V ↦ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ⟨ ⟨ 𝑥 , 𝑧 ⟩ , 𝑦 ⟩ ∈ 𝑤 } )