Metamath Proof Explorer

Theorem gdlopcfv7

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

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

Proof

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