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 | |- ~F8 = ( x e. _V , y e. _V |-> ( x i^i ( Cnv3 ` y ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cgdlop8 | |- ~F8 |
|
| 1 | vx | |- x |
|
| 2 | cvv | |- _V |
|
| 3 | vy | |- y |
|
| 4 | 1 | cv | |- x |
| 5 | ccnv3 | |- Cnv3 |
|
| 6 | 3 | cv | |- y |
| 7 | 6 5 | cfv | |- ( Cnv3 ` y ) |
| 8 | 4 7 | cin | |- ( x i^i ( Cnv3 ` y ) ) |
| 9 | 1 3 2 2 8 | cmpo | |- ( x e. _V , y e. _V |-> ( x i^i ( Cnv3 ` y ) ) ) |
| 10 | 0 9 | wceq | |- ~F8 = ( x e. _V , y e. _V |-> ( x i^i ( Cnv3 ` y ) ) ) |