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	Could not format assertion : No typesetting found for |- Cnv2 = ( w e. _V |-> { <. <. x , y >. , z >. | <. <. z , x >. , y >. e. w } ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnv2	Could not format Cnv2 : No typesetting found for class Cnv2 with typecode class
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		vy	$$setvary$$
5		vz	$$setvarz$$
6	5	cv	$$setvarz$$
7	3	cv	$$setvarx$$
8	6 7	cop	$$class⟨z,x⟩$$
9	4	cv	$$setvary$$
10	8 9	cop	$$class⟨⟨z,x⟩,y⟩$$
11	1	cv	$$setvarw$$
12	10 11	wcel	$$wff⟨⟨z,x⟩,y⟩\in w$$
13	12 3 4 5	coprab	$$class\left\{⟨⟨x,y⟩,z⟩|⟨⟨z,x⟩,y⟩\in w\right\}$$
14	1 2 13	cmpt	$$class\left(w\in \mathrm{V}⟼\left\{⟨⟨x,y⟩,z⟩|⟨⟨z,x⟩,y⟩\in w\right\}\right)$$
15	0 14	wceq	Could not format Cnv2 = ( w e. _V |-> { <. <. x , y >. , z >. | <. <. z , x >. , y >. e. w } ) : No typesetting found for wff Cnv2 = ( w e. _V |-> { <. <. x , y >. , z >. | <. <. z , x >. , y >. e. w } ) with typecode wff