Definition df-gdlop8

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

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

Detailed syntax breakdown

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