Metamath Proof Explorer

Theorem gdlopcfv2

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

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

Proof

Step Hyp Ref Expression
1 gdlopcfv2.1 
 |-  ( ph -> A e. V )
2 gdlopcfv2.2 
 |-  ( ph -> B e. W )
3 2olt9o 
 |-  2o e. 9o
4 df-2o 
 |-  2o = suc 1o
5 3 4 suceldifsn0 
 |-  2o e. ( 9o \ { (/) } )
6 5 a1i 
 |-  ( ph -> 2o e. ( 9o \ { (/) } ) )
7 1 elexd 
 |-  ( ph -> A e. _V )
8 2 elexd 
 |-  ( ph -> B e. _V )
9 fvexd 
 |-  ( ph -> ( ~F2 ` <. A , B >. ) e. _V )
10 1on 
 |-  1o e. On
11 2on 
 |-  2o e. On
12 10 4 eqsucidi 
 |-  1o e. 2o
13 10 11 12 gdlopcfvlem 
 |-  ( ( ph /\ 2o = 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 >. ) ) ) ) ) ) ) )
14 eqcom 
 |-  ( 2o = n <-> n = 2o )
15 14 bilani 
 |-  ( ( ph /\ 2o = n ) -> n = 2o )
16 15 iftrued 
 |-  ( ( ph /\ 2o = 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 >. ) ) ) ) ) ) ) = ( ~F2 ` <. x , y >. ) )
17 13 16 eqtr2d 
 |-  ( ( ph /\ 2o = n ) -> ( ~F2 ` <. 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 >. ) ) ) ) ) ) ) ) )
18 opeq1 
 |-  ( A = x -> <. A , y >. = <. x , y >. )
19 18 fveq2d 
 |-  ( A = x -> ( ~F2 ` <. A , y >. ) = ( ~F2 ` <. x , y >. ) )
20 19 adantl 
 |-  ( ( ph /\ A = x ) -> ( ~F2 ` <. A , y >. ) = ( ~F2 ` <. x , y >. ) )
21 opeq2 
 |-  ( B = y -> <. A , B >. = <. A , y >. )
22 21 fveq2d 
 |-  ( B = y -> ( ~F2 ` <. A , B >. ) = ( ~F2 ` <. A , y >. ) )
23 22 adantl 
 |-  ( ( ph /\ B = y ) -> ( ~F2 ` <. A , B >. ) = ( ~F2 ` <. A , y >. ) )
24 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 >. ) ) ) ) ) ) ) ) )
25 6 7 8 9 17 20 23 24 mpt3fvot2d 
 |-  ( ph -> ( ~F ` <. 2o , A , B >. ) = ( ~F2 ` <. A , B >. ) )
26 1 2 gdlop2fv 
 |-  ( ph -> ( ~F2 ` <. A , B >. ) = ( A i^i _E ) )
27 25 26 eqtrd 
 |-  ( ph -> ( ~F ` <. 2o , A , B >. ) = ( A i^i _E ) )