Definition df-gdlopc 35911

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 35903 through df-gdlop8 35910 to apply to the second and third arguments. Based on Definition 14.2 of [TakeutiZaring] p. 144. (Contributed by BTernaryTau, 2-Sep-2026.)

Assertion

Ref	Expression
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‘⟨𝑥, 𝑦⟩)))))))))

Distinct variable group:   𝑥,𝑛,𝑦

Detailed syntax breakdown of Definition df-gdlopc

Step	Hyp	Ref	Expression
1		cgdlopc 35900	. 2 class ℱ
2		vn	. . 3 setvar 𝑛
3		vx	. . 3 setvar 𝑥
4		vy	. . 3 setvar 𝑦
5		c9o 35814	. . . 4 class 9o
6		c0 4278	. . . . 5 class ∅
7	6	csn 4583	. . . 4 class {∅}
8	5, 7	cdif 4045	. . 3 class (9o ∖ {∅})
9		cvv 3450	. . 3 class V
10	2	cv 1568	. . . . 5 class 𝑛
11		c1o 8470	. . . . 5 class 1o
12	10, 11	wceq 1569	. . . 4 wff 𝑛 = 1o
13	3	cv 1568	. . . . . 6 class 𝑥
14	4	cv 1568	. . . . . 6 class 𝑦
15	13, 14	cop 4589	. . . . 5 class ⟨𝑥, 𝑦⟩
16		cgdlop1 35892	. . . . 5 class ℱ1
17	15, 16	cfv 6538	. . . 4 class (ℱ1‘⟨𝑥, 𝑦⟩)
18		c2o 8471	. . . . . 6 class 2o
19	10, 18	wceq 1569	. . . . 5 wff 𝑛 = 2o
20		cgdlop2 35893	. . . . . 6 class ℱ2
21	15, 20	cfv 6538	. . . . 5 class (ℱ2‘⟨𝑥, 𝑦⟩)
22		c3o 8472	. . . . . . 7 class 3o
23	10, 22	wceq 1569	. . . . . 6 wff 𝑛 = 3o
24		cgdlop3 35894	. . . . . . 7 class ℱ3
25	15, 24	cfv 6538	. . . . . 6 class (ℱ3‘⟨𝑥, 𝑦⟩)
26		c4o 8473	. . . . . . . 8 class 4o
27	10, 26	wceq 1569	. . . . . . 7 wff 𝑛 = 4o
28		cgdlop4 35895	. . . . . . . 8 class ℱ4
29	15, 28	cfv 6538	. . . . . . 7 class (ℱ4‘⟨𝑥, 𝑦⟩)
30		c5o 35810	. . . . . . . . 9 class 5o
31	10, 30	wceq 1569	. . . . . . . 8 wff 𝑛 = 5o
32		cgdlop5 35896	. . . . . . . . 9 class ℱ5
33	15, 32	cfv 6538	. . . . . . . 8 class (ℱ5‘⟨𝑥, 𝑦⟩)
34		c6o 35811	. . . . . . . . . 10 class 6o
35	10, 34	wceq 1569	. . . . . . . . 9 wff 𝑛 = 6o
36		cgdlop6 35897	. . . . . . . . . 10 class ℱ6
37	15, 36	cfv 6538	. . . . . . . . 9 class (ℱ6‘⟨𝑥, 𝑦⟩)
38		c7o 35812	. . . . . . . . . . 11 class 7o
39	10, 38	wceq 1569	. . . . . . . . . 10 wff 𝑛 = 7o
40		cgdlop7 35898	. . . . . . . . . . 11 class ℱ7
41	15, 40	cfv 6538	. . . . . . . . . 10 class (ℱ7‘⟨𝑥, 𝑦⟩)
42		cgdlop8 35899	. . . . . . . . . . 11 class ℱ8
43	15, 42	cfv 6538	. . . . . . . . . 10 class (ℱ8‘⟨𝑥, 𝑦⟩)
44	39, 41, 43	cif 4481	. . . . . . . . 9 class if(𝑛 = 7o, (ℱ7‘⟨𝑥, 𝑦⟩), (ℱ8‘⟨𝑥, 𝑦⟩))
45	35, 37, 44	cif 4481	. . . . . . . 8 class if(𝑛 = 6o, (ℱ6‘⟨𝑥, 𝑦⟩), if(𝑛 = 7o, (ℱ7‘⟨𝑥, 𝑦⟩), (ℱ8‘⟨𝑥, 𝑦⟩)))
46	31, 33, 45	cif 4481	. . . . . . 7 class if(𝑛 = 5o, (ℱ5‘⟨𝑥, 𝑦⟩), if(𝑛 = 6o, (ℱ6‘⟨𝑥, 𝑦⟩), if(𝑛 = 7o, (ℱ7‘⟨𝑥, 𝑦⟩), (ℱ8‘⟨𝑥, 𝑦⟩))))
47	27, 29, 46	cif 4481	. . . . . 6 class if(𝑛 = 4o, (ℱ4‘⟨𝑥, 𝑦⟩), if(𝑛 = 5o, (ℱ5‘⟨𝑥, 𝑦⟩), if(𝑛 = 6o, (ℱ6‘⟨𝑥, 𝑦⟩), if(𝑛 = 7o, (ℱ7‘⟨𝑥, 𝑦⟩), (ℱ8‘⟨𝑥, 𝑦⟩)))))
48	23, 25, 47	cif 4481	. . . . 5 class if(𝑛 = 3o, (ℱ3‘⟨𝑥, 𝑦⟩), if(𝑛 = 4o, (ℱ4‘⟨𝑥, 𝑦⟩), if(𝑛 = 5o, (ℱ5‘⟨𝑥, 𝑦⟩), if(𝑛 = 6o, (ℱ6‘⟨𝑥, 𝑦⟩), if(𝑛 = 7o, (ℱ7‘⟨𝑥, 𝑦⟩), (ℱ8‘⟨𝑥, 𝑦⟩))))))
49	19, 21, 48	cif 4481	. . . 4 class if(𝑛 = 2o, (ℱ2‘⟨𝑥, 𝑦⟩), if(𝑛 = 3o, (ℱ3‘⟨𝑥, 𝑦⟩), if(𝑛 = 4o, (ℱ4‘⟨𝑥, 𝑦⟩), if(𝑛 = 5o, (ℱ5‘⟨𝑥, 𝑦⟩), if(𝑛 = 6o, (ℱ6‘⟨𝑥, 𝑦⟩), if(𝑛 = 7o, (ℱ7‘⟨𝑥, 𝑦⟩), (ℱ8‘⟨𝑥, 𝑦⟩)))))))
50	12, 17, 49	cif 4481	. . 3 class if(𝑛 = 1o, (ℱ1‘⟨𝑥, 𝑦⟩), if(𝑛 = 2o, (ℱ2‘⟨𝑥, 𝑦⟩), if(𝑛 = 3o, (ℱ3‘⟨𝑥, 𝑦⟩), if(𝑛 = 4o, (ℱ4‘⟨𝑥, 𝑦⟩), if(𝑛 = 5o, (ℱ5‘⟨𝑥, 𝑦⟩), if(𝑛 = 6o, (ℱ6‘⟨𝑥, 𝑦⟩), if(𝑛 = 7o, (ℱ7‘⟨𝑥, 𝑦⟩), (ℱ8‘⟨𝑥, 𝑦⟩))))))))
51	2, 3, 4, 8, 9, 9, 50	cmpt3 7683	. 2 class (𝑛 ∈ (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‘⟨𝑥, 𝑦⟩)))))))))
52	1, 51	wceq 1569	1 wff ℱ = (𝑛 ∈ (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‘⟨𝑥, 𝑦⟩)))))))))

This definition is used by: (None)