Metamath Proof Explorer

Theorem gdlopcfv5

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

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

Proof

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