Definition df-gdlopc

Description: Define the combined Gödel operations. This function takes three arguments and uses the first to determine which of the eight Gödel operations df-gdlop1 through df-gdlop8 to apply to the second and third arguments. Based on Definition 14.2 of TakeutiZaring p. 144. (Contributed by BTernaryTau, 2-Sep-2026)

	Ref	Expression
Assertion	df-gdlopc	Could not format assertion : No typesetting found for |- ~F = ( n e. ( 9o \ { (/) } ) , x e. _V , y e. _V |-> if ( n = 1o , ( ~F1 ` <. x , y >. ) , if ( n = 2o , ( ~F2 ` <. x , y >. ) , if ( n = 3o , ( ~F3 ` <. x , y >. ) , if ( n = 4o , ( ~F4 ` <. x , y >. ) , if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) ) ) ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgdlopc	Could not format ~F : No typesetting found for class ~F with typecode class
1		vn	$$setvarn$$
2		c9o	Could not format 9o : No typesetting found for class 9o with typecode class
3		c0	$$class\varnothing$$
4	3	csn	$$class\left\{\varnothing \right\}$$
5	2 4	cdif	Could not format ( 9o \ { (/) } ) : No typesetting found for class ( 9o \ { (/) } ) with typecode class
6		vx	$$setvarx$$
7		cvv	$$class\mathrm{V}$$
8		vy	$$setvary$$
9	1	cv	$$setvarn$$
10		c1o	$$class{1}_{𝑜}$$
11	9 10	wceq	$$wffn=1_{𝑜}$$
12		cgdlop1	Could not format ~F1 : No typesetting found for class ~F1 with typecode class
13	6	cv	$$setvarx$$
14	8	cv	$$setvary$$
15	13 14	cop	$$class⟨x,y⟩$$
16	15 12	cfv	Could not format ( ~F1 ` <. x , y >. ) : No typesetting found for class ( ~F1 ` <. x , y >. ) with typecode class
17		c2o	$$class{2}_{𝑜}$$
18	9 17	wceq	$$wffn=2_{𝑜}$$
19		cgdlop2	Could not format ~F2 : No typesetting found for class ~F2 with typecode class
20	15 19	cfv	Could not format ( ~F2 ` <. x , y >. ) : No typesetting found for class ( ~F2 ` <. x , y >. ) with typecode class
21		c3o	$$class{3}_{𝑜}$$
22	9 21	wceq	$$wffn=3_{𝑜}$$
23		cgdlop3	Could not format ~F3 : No typesetting found for class ~F3 with typecode class
24	15 23	cfv	Could not format ( ~F3 ` <. x , y >. ) : No typesetting found for class ( ~F3 ` <. x , y >. ) with typecode class
25		c4o	$$class{4}_{𝑜}$$
26	9 25	wceq	$$wffn=4_{𝑜}$$
27		cgdlop4	Could not format ~F4 : No typesetting found for class ~F4 with typecode class
28	15 27	cfv	Could not format ( ~F4 ` <. x , y >. ) : No typesetting found for class ( ~F4 ` <. x , y >. ) with typecode class
29		c5o	Could not format 5o : No typesetting found for class 5o with typecode class
30	9 29	wceq	Could not format n = 5o : No typesetting found for wff n = 5o with typecode wff
31		cgdlop5	Could not format ~F5 : No typesetting found for class ~F5 with typecode class
32	15 31	cfv	Could not format ( ~F5 ` <. x , y >. ) : No typesetting found for class ( ~F5 ` <. x , y >. ) with typecode class
33		c6o	Could not format 6o : No typesetting found for class 6o with typecode class
34	9 33	wceq	Could not format n = 6o : No typesetting found for wff n = 6o with typecode wff
35		cgdlop6	Could not format ~F6 : No typesetting found for class ~F6 with typecode class
36	15 35	cfv	Could not format ( ~F6 ` <. x , y >. ) : No typesetting found for class ( ~F6 ` <. x , y >. ) with typecode class
37		c7o	Could not format 7o : No typesetting found for class 7o with typecode class
38	9 37	wceq	Could not format n = 7o : No typesetting found for wff n = 7o with typecode wff
39		cgdlop7	Could not format ~F7 : No typesetting found for class ~F7 with typecode class
40	15 39	cfv	Could not format ( ~F7 ` <. x , y >. ) : No typesetting found for class ( ~F7 ` <. x , y >. ) with typecode class
41		cgdlop8	Could not format ~F8 : No typesetting found for class ~F8 with typecode class
42	15 41	cfv	Could not format ( ~F8 ` <. x , y >. ) : No typesetting found for class ( ~F8 ` <. x , y >. ) with typecode class
43	38 40 42	cif	Could not format if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) : No typesetting found for class if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) with typecode class
44	34 36 43	cif	Could not format if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) : No typesetting found for class if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) with typecode class
45	30 32 44	cif	Could not format if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) : No typesetting found for class if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) with typecode class
46	26 28 45	cif	Could not format if ( n = 4o , ( ~F4 ` <. x , y >. ) , if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) ) : No typesetting found for class if ( n = 4o , ( ~F4 ` <. x , y >. ) , if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) ) with typecode class
47	22 24 46	cif	Could not format if ( n = 3o , ( ~F3 ` <. x , y >. ) , if ( n = 4o , ( ~F4 ` <. x , y >. ) , if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) ) ) : No typesetting found for class if ( n = 3o , ( ~F3 ` <. x , y >. ) , if ( n = 4o , ( ~F4 ` <. x , y >. ) , if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) ) ) with typecode class
48	18 20 47	cif	Could not format if ( n = 2o , ( ~F2 ` <. x , y >. ) , if ( n = 3o , ( ~F3 ` <. x , y >. ) , if ( n = 4o , ( ~F4 ` <. x , y >. ) , if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) ) ) ) : No typesetting found for class if ( n = 2o , ( ~F2 ` <. x , y >. ) , if ( n = 3o , ( ~F3 ` <. x , y >. ) , if ( n = 4o , ( ~F4 ` <. x , y >. ) , if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) ) ) ) with typecode class
49	11 16 48	cif	Could not format if ( n = 1o , ( ~F1 ` <. x , y >. ) , if ( n = 2o , ( ~F2 ` <. x , y >. ) , if ( n = 3o , ( ~F3 ` <. x , y >. ) , if ( n = 4o , ( ~F4 ` <. x , y >. ) , if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) ) ) ) ) : No typesetting found for class if ( n = 1o , ( ~F1 ` <. x , y >. ) , if ( n = 2o , ( ~F2 ` <. x , y >. ) , if ( n = 3o , ( ~F3 ` <. x , y >. ) , if ( n = 4o , ( ~F4 ` <. x , y >. ) , if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) ) ) ) ) with typecode class
50	1 6 8 5 7 7 49	cmpt3	Could not format ( n e. ( 9o \ { (/) } ) , x e. _V , y e. _V |-> if ( n = 1o , ( ~F1 ` <. x , y >. ) , if ( n = 2o , ( ~F2 ` <. x , y >. ) , if ( n = 3o , ( ~F3 ` <. x , y >. ) , if ( n = 4o , ( ~F4 ` <. x , y >. ) , if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) ) ) ) ) ) : No typesetting found for class ( n e. ( 9o \ { (/) } ) , x e. _V , y e. _V |-> if ( n = 1o , ( ~F1 ` <. x , y >. ) , if ( n = 2o , ( ~F2 ` <. x , y >. ) , if ( n = 3o , ( ~F3 ` <. x , y >. ) , if ( n = 4o , ( ~F4 ` <. x , y >. ) , if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) ) ) ) ) ) with typecode class
51	0 50	wceq	Could not format ~F = ( n e. ( 9o \ { (/) } ) , x e. _V , y e. _V |-> if ( n = 1o , ( ~F1 ` <. x , y >. ) , if ( n = 2o , ( ~F2 ` <. x , y >. ) , if ( n = 3o , ( ~F3 ` <. x , y >. ) , if ( n = 4o , ( ~F4 ` <. x , y >. ) , if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) ) ) ) ) ) : No typesetting found for wff ~F = ( n e. ( 9o \ { (/) } ) , x e. _V , y e. _V |-> if ( n = 1o , ( ~F1 ` <. x , y >. ) , if ( n = 2o , ( ~F2 ` <. x , y >. ) , if ( n = 3o , ( ~F3 ` <. x , y >. ) , if ( n = 4o , ( ~F4 ` <. x , y >. ) , if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) ) ) ) ) ) with typecode wff