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

Detailed syntax breakdown

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