Metamath Proof Explorer

Theorem gdlopcfv8

Description: The value of the combined Gödel operations function when its first argument is 8. (Contributed by BTernaryTau, 19-Oct-2026)

Ref Expression
Hypotheses gdlopcfv8.1 
|- ( ph -> A e. V )
gdlopcfv8.2 
|- ( ph -> B e. W )
Assertion gdlopcfv8 
|- ( ph -> ( ~F ` <. 8o , A , B >. ) = ( A i^i ( Cnv3 ` B ) ) )

Proof

Step Hyp Ref Expression
1 gdlopcfv8.1 
 |-  ( ph -> A e. V )
2 gdlopcfv8.2 
 |-  ( ph -> B e. W )
3 8olt9o 
 |-  8o e. 9o
4 df-8o 
 |-  8o = suc 7o
5 3 4 suceldifsn0 
 |-  8o e. ( 9o \ { (/) } )
6 5 a1i 
 |-  ( ph -> 8o e. ( 9o \ { (/) } ) )
7 1 elexd 
 |-  ( ph -> A e. _V )
8 2 elexd 
 |-  ( ph -> B e. _V )
9 fvexd 
 |-  ( ph -> ( ~F8 ` <. A , B >. ) e. _V )
10 2on 
 |-  2o e. On
11 8on 
 |-  8o e. On
12 df-3o 
 |-  3o = suc 2o
13 10 12 eqsucidi 
 |-  2o e. 3o
14 3on 
 |-  3o e. On
15 df-4o 
 |-  4o = suc 3o
16 14 15 eqsucidi 
 |-  3o e. 4o
17 4on 
 |-  4o e. On
18 df-5o 
 |-  5o = suc 4o
19 17 18 eqsucidi 
 |-  4o e. 5o
20 5on 
 |-  5o e. On
21 df-6o 
 |-  6o = suc 5o
22 20 21 eqsucidi 
 |-  5o e. 6o
23 6on 
 |-  6o e. On
24 df-7o 
 |-  7o = suc 6o
25 23 24 eqsucidi 
 |-  6o e. 7o
26 7on 
 |-  7o e. On
27 26 4 eqsucidi 
 |-  7o e. 8o
28 11 25 27 ontr1i 
 |-  6o e. 8o
29 11 22 28 ontr1i 
 |-  5o e. 8o
30 11 19 29 ontr1i 
 |-  4o e. 8o
31 11 16 30 ontr1i 
 |-  3o e. 8o
32 11 13 31 ontr1i 
 |-  2o e. 8o
33 10 11 32 gdlopcfvlem 
 |-  ( ( ph /\ 8o = n ) -> 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 >. ) ) ) ) ) ) ) = 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 >. ) ) ) ) ) ) )
34 1on 
 |-  1o e. On
35 df-2o 
 |-  2o = suc 1o
36 34 35 eqsucidi 
 |-  1o e. 2o
37 11 36 32 ontr1i 
 |-  1o e. 8o
38 34 11 37 gdlopcfvlem 
 |-  ( ( ph /\ 8o = n ) -> 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 >. ) ) ) ) ) ) ) ) = 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 >. ) ) ) ) ) ) ) )
39 17 11 30 gdlopcfvlem 
 |-  ( ( ph /\ 8o = n ) -> 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 >. ) ) ) ) ) = if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) )
40 14 11 31 gdlopcfvlem 
 |-  ( ( ph /\ 8o = n ) -> 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 >. ) ) ) ) ) ) = 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 >. ) ) ) ) ) )
41 20 11 29 gdlopcfvlem 
 |-  ( ( ph /\ 8o = n ) -> if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) = if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) )
42 23 11 28 gdlopcfvlem 
 |-  ( ( ph /\ 8o = n ) -> if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) = if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) )
43 26 11 27 gdlopcfvlem 
 |-  ( ( ph /\ 8o = n ) -> if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) = ( ~F8 ` <. x , y >. ) )
44 41 42 43 3eqtrrd 
 |-  ( ( ph /\ 8o = n ) -> ( ~F8 ` <. x , y >. ) = if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) )
45 39 40 44 3eqtr4rd 
 |-  ( ( ph /\ 8o = n ) -> ( ~F8 ` <. 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 >. ) ) ) ) ) ) )
46 33 38 45 3eqtr4rd 
 |-  ( ( ph /\ 8o = n ) -> ( ~F8 ` <. x , y >. ) = 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 >. ) ) ) ) ) ) ) ) )
47 opeq1 
 |-  ( A = x -> <. A , y >. = <. x , y >. )
48 47 fveq2d 
 |-  ( A = x -> ( ~F8 ` <. A , y >. ) = ( ~F8 ` <. x , y >. ) )
49 48 adantl 
 |-  ( ( ph /\ A = x ) -> ( ~F8 ` <. A , y >. ) = ( ~F8 ` <. x , y >. ) )
50 opeq2 
 |-  ( B = y -> <. A , B >. = <. A , y >. )
51 50 fveq2d 
 |-  ( B = y -> ( ~F8 ` <. A , B >. ) = ( ~F8 ` <. A , y >. ) )
52 51 adantl 
 |-  ( ( ph /\ B = y ) -> ( ~F8 ` <. A , B >. ) = ( ~F8 ` <. A , y >. ) )
53 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 >. ) ) ) ) ) ) ) ) )
54 6 7 8 9 46 49 52 53 mpt3fvot2d 
 |-  ( ph -> ( ~F ` <. 8o , A , B >. ) = ( ~F8 ` <. A , B >. ) )
55 1 2 gdlop8fv 
 |-  ( ph -> ( ~F8 ` <. A , B >. ) = ( A i^i ( Cnv3 ` B ) ) )
56 54 55 eqtrd 
 |-  ( ph -> ( ~F ` <. 8o , A , B >. ) = ( A i^i ( Cnv3 ` B ) ) )