Metamath Proof Explorer

Theorem gdlopcfv4

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

Ref Expression
Hypotheses gdlopcfv4.1 
|- ( ph -> A e. V )
gdlopcfv4.2 
|- ( ph -> B e. W )
Assertion gdlopcfv4 
|- ( ph -> ( ~F ` <. 4o , A , B >. ) = ( A |` B ) )

Proof

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