Definition df-gdlop7

Description: Define the seventh Gödel operation. This function takes two arguments and returns the intersection of the first argument with the second converse of the second argument (see df-in and df-cnv2 ). Based on the seventh case of Definition 14.2 of TakeutiZaring p. 144. (Contributed by BTernaryTau, 2-Sep-2026)

	Ref	Expression
Assertion	df-gdlop7	Could not format assertion : No typesetting found for |- ~F7 = ( x e. _V , y e. _V |-> ( x i^i ( Cnv2 ` y ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgdlop7	Could not format ~F7 : No typesetting found for class ~F7 with typecode class
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vy	$$setvary$$
4	1	cv	$$setvarx$$
5		ccnv2	Could not format Cnv2 : No typesetting found for class Cnv2 with typecode class
6	3	cv	$$setvary$$
7	6 5	cfv	Could not format ( Cnv2 ` y ) : No typesetting found for class ( Cnv2 ` y ) with typecode class
8	4 7	cin	Could not format ( x i^i ( Cnv2 ` y ) ) : No typesetting found for class ( x i^i ( Cnv2 ` y ) ) with typecode class
9	1 3 2 2 8	cmpo	Could not format ( x e. _V , y e. _V |-> ( x i^i ( Cnv2 ` y ) ) ) : No typesetting found for class ( x e. _V , y e. _V |-> ( x i^i ( Cnv2 ` y ) ) ) with typecode class
10	0 9	wceq	Could not format ~F7 = ( x e. _V , y e. _V |-> ( x i^i ( Cnv2 ` y ) ) ) : No typesetting found for wff ~F7 = ( x e. _V , y e. _V |-> ( x i^i ( Cnv2 ` y ) ) ) with typecode wff