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 = ( w e. _V |-> { <. <. x , y >. , z >. | <. <. z , x >. , y >. e. w } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnv2	|- Cnv2
1		vw	|- w
2		cvv	|- _V
3		vx	|- x
4		vy	|- y
5		vz	|- z
6	5	cv	|- z
7	3	cv	|- x
8	6 7	cop	|- <. z , x >.
9	4	cv	|- y
10	8 9	cop	|- <. <. z , x >. , y >.
11	1	cv	|- w
12	10 11	wcel	|- <. <. z , x >. , y >. e. w
13	12 3 4 5	coprab	|- { <. <. x , y >. , z >. | <. <. z , x >. , y >. e. w }
14	1 2 13	cmpt	|- ( w e. _V |-> { <. <. x , y >. , z >. | <. <. z , x >. , y >. e. w } )
15	0 14	wceq	|- Cnv2 = ( w e. _V |-> { <. <. x , y >. , z >. | <. <. z , x >. , y >. e. w } )