Definition df-cnv2

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnv2	⊢ Cnv2
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		vy	⊢ 𝑦
5		vz	⊢ 𝑧
6	5	cv	⊢ 𝑧
7	3	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	⊢ Cnv2 = ( 𝑤 ∈ V ↦ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ⟨ ⟨ 𝑧 , 𝑥 ⟩ , 𝑦 ⟩ ∈ 𝑤 } )