Metamath Proof Explorer

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 
|- ~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 >. ) ) ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgdlopc 
 |-  ~F
1 vn 
 |-  n
2 c9o 
 |-  9o
3 c0 
 |-  (/)
4 3 csn 
 |-  { (/) }
5 2 4 cdif 
 |-  ( 9o \ { (/) } )
6 vx 
 |-  x
7 cvv 
 |-  _V
8 vy 
 |-  y
9 1 cv 
 |-  n
10 c1o 
 |-  1o
11 9 10 wceq 
 |-  n = 1o
12 cgdlop1 
 |-  ~F1
13 6 cv 
 |-  x
14 8 cv 
 |-  y
15 13 14 cop 
 |-  <. x , y >.
16 15 12 cfv 
 |-  ( ~F1 ` <. x , y >. )
17 c2o 
 |-  2o
18 9 17 wceq 
 |-  n = 2o
19 cgdlop2 
 |-  ~F2
20 15 19 cfv 
 |-  ( ~F2 ` <. x , y >. )
21 c3o 
 |-  3o
22 9 21 wceq 
 |-  n = 3o
23 cgdlop3 
 |-  ~F3
24 15 23 cfv 
 |-  ( ~F3 ` <. x , y >. )
25 c4o 
 |-  4o
26 9 25 wceq 
 |-  n = 4o
27 cgdlop4 
 |-  ~F4
28 15 27 cfv 
 |-  ( ~F4 ` <. x , y >. )
29 c5o 
 |-  5o
30 9 29 wceq 
 |-  n = 5o
31 cgdlop5 
 |-  ~F5
32 15 31 cfv 
 |-  ( ~F5 ` <. x , y >. )
33 c6o 
 |-  6o
34 9 33 wceq 
 |-  n = 6o
35 cgdlop6 
 |-  ~F6
36 15 35 cfv 
 |-  ( ~F6 ` <. x , y >. )
37 c7o 
 |-  7o
38 9 37 wceq 
 |-  n = 7o
39 cgdlop7 
 |-  ~F7
40 15 39 cfv 
 |-  ( ~F7 ` <. x , y >. )
41 cgdlop8 
 |-  ~F8
42 15 41 cfv 
 |-  ( ~F8 ` <. x , y >. )
43 38 40 42 cif 
 |-  if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) )
44 34 36 43 cif 
 |-  if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) )
45 30 32 44 cif 
 |-  if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) )
46 26 28 45 cif 
 |-  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 >. ) ) ) ) )
47 22 24 46 cif 
 |-  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 >. ) ) ) ) ) )
48 18 20 47 cif 
 |-  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 >. ) ) ) ) ) ) )
49 11 16 48 cif 
 |-  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 >. ) ) ) ) ) ) ) )
50 1 6 8 5 7 7 49 cmpt3 
 |-  ( 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 >. ) ) ) ) ) ) ) ) )
51 0 50 wceq 
 |-  ~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 >. ) ) ) ) ) ) ) ) )