Metamath Proof Explorer

Theorem gdlopcfv6

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

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

Proof

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