Metamath Proof Explorer

Theorem gdlopcfv1

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

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

Proof

Step Hyp Ref Expression
1 gdlopcfv1.1 
 |-  ( ph -> A e. V )
2 gdlopcfv1.2 
 |-  ( ph -> B e. W )
3 1olt9o 
 |-  1o e. 9o
4 df-1o 
 |-  1o = suc (/)
5 3 4 suceldifsn0 
 |-  1o e. ( 9o \ { (/) } )
6 5 a1i 
 |-  ( ph -> 1o e. ( 9o \ { (/) } ) )
7 1 elexd 
 |-  ( ph -> A e. _V )
8 2 elexd 
 |-  ( ph -> B e. _V )
9 fvexd 
 |-  ( ph -> ( ~F1 ` <. A , B >. ) e. _V )
10 eqcom 
 |-  ( 1o = n <-> n = 1o )
11 10 bilani 
 |-  ( ( ph /\ 1o = n ) -> n = 1o )
12 11 iftrued 
 |-  ( ( ph /\ 1o = 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 >. ) ) ) ) ) ) ) ) = ( ~F1 ` <. x , y >. ) )
13 12 eqcomd 
 |-  ( ( ph /\ 1o = n ) -> ( ~F1 ` <. 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 >. ) ) ) ) ) ) ) ) )
14 opeq1 
 |-  ( A = x -> <. A , y >. = <. x , y >. )
15 14 fveq2d 
 |-  ( A = x -> ( ~F1 ` <. A , y >. ) = ( ~F1 ` <. x , y >. ) )
16 15 adantl 
 |-  ( ( ph /\ A = x ) -> ( ~F1 ` <. A , y >. ) = ( ~F1 ` <. x , y >. ) )
17 opeq2 
 |-  ( B = y -> <. A , B >. = <. A , y >. )
18 17 fveq2d 
 |-  ( B = y -> ( ~F1 ` <. A , B >. ) = ( ~F1 ` <. A , y >. ) )
19 18 adantl 
 |-  ( ( ph /\ B = y ) -> ( ~F1 ` <. A , B >. ) = ( ~F1 ` <. A , y >. ) )
20 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 >. ) ) ) ) ) ) ) ) )
21 6 7 8 9 13 16 19 20 mpt3fvot2d 
 |-  ( ph -> ( ~F ` <. 1o , A , B >. ) = ( ~F1 ` <. A , B >. ) )
22 1 2 gdlop1fv 
 |-  ( ph -> ( ~F1 ` <. A , B >. ) = { A , B } )
23 21 22 eqtrd 
 |-  ( ph -> ( ~F ` <. 1o , A , B >. ) = { A , B } )