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	⊢ ℱ = ( 𝑛 ∈ ( 9o ∖ { ∅ } ) , 𝑥 ∈ V , 𝑦 ∈ V ↦ if ( 𝑛 = 1o , ( ℱ1 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 2o , ( ℱ2 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3o , ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgdlopc	⊢ ℱ
1		vn	⊢ 𝑛
2		c9o	⊢ 9o
3		c0	⊢ ∅
4	3	csn	⊢ { ∅ }
5	2 4	cdif	⊢ ( 9o ∖ { ∅ } )
6		vx	⊢ 𝑥
7		cvv	⊢ V
8		vy	⊢ 𝑦
9	1	cv	⊢ 𝑛
10		c1o	⊢ 1o
11	9 10	wceq	⊢ 𝑛 = 1o
12		cgdlop1	⊢ ℱ1
13	6	cv	⊢ 𝑥
14	8	cv	⊢ 𝑦
15	13 14	cop	⊢ ⟨ 𝑥 , 𝑦 ⟩
16	15 12	cfv	⊢ ( ℱ1 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
17		c2o	⊢ 2o
18	9 17	wceq	⊢ 𝑛 = 2o
19		cgdlop2	⊢ ℱ2
20	15 19	cfv	⊢ ( ℱ2 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
21		c3o	⊢ 3o
22	9 21	wceq	⊢ 𝑛 = 3o
23		cgdlop3	⊢ ℱ3
24	15 23	cfv	⊢ ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
25		c4o	⊢ 4o
26	9 25	wceq	⊢ 𝑛 = 4o
27		cgdlop4	⊢ ℱ4
28	15 27	cfv	⊢ ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
29		c5o	⊢ 5o
30	9 29	wceq	⊢ 𝑛 = 5o
31		cgdlop5	⊢ ℱ5
32	15 31	cfv	⊢ ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
33		c6o	⊢ 6o
34	9 33	wceq	⊢ 𝑛 = 6o
35		cgdlop6	⊢ ℱ6
36	15 35	cfv	⊢ ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
37		c7o	⊢ 7o
38	9 37	wceq	⊢ 𝑛 = 7o
39		cgdlop7	⊢ ℱ7
40	15 39	cfv	⊢ ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
41		cgdlop8	⊢ ℱ8
42	15 41	cfv	⊢ ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
43	38 40 42	cif	⊢ if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
44	34 36 43	cif	⊢ if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
45	30 32 44	cif	⊢ if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) )
46	26 28 45	cif	⊢ if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) )
47	22 24 46	cif	⊢ if ( 𝑛 = 3o , ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) )
48	18 20 47	cif	⊢ if ( 𝑛 = 2o , ( ℱ2 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3o , ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) )
49	11 16 48	cif	⊢ if ( 𝑛 = 1o , ( ℱ1 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 2o , ( ℱ2 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3o , ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) )
50	1 6 8 5 7 7 49	cmpt3	⊢ ( 𝑛 ∈ ( 9o ∖ { ∅ } ) , 𝑥 ∈ V , 𝑦 ∈ V ↦ if ( 𝑛 = 1o , ( ℱ1 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 2o , ( ℱ2 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3o , ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) ) )
51	0 50	wceq	⊢ ℱ = ( 𝑛 ∈ ( 9o ∖ { ∅ } ) , 𝑥 ∈ V , 𝑦 ∈ V ↦ if ( 𝑛 = 1o , ( ℱ1 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 2o , ( ℱ2 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 3o , ( ℱ3 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 4o , ( ℱ4 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 5o , ( ℱ5 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 6o , ( ℱ6 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , if ( 𝑛 = 7o , ( ℱ7 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ℱ8 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) ) ) ) ) ) ) )