Theorem gdlopcfv8

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

	Ref	Expression
Hypotheses	gdlopcfv8.1	$$⊢\phi \to A\in V$$
	gdlopcfv8.2	$$⊢\phi \to B\in W$$
Assertion	gdlopcfv8	Could not format assertion : No typesetting found for |- ( ph -> ( ~F ` <. 8o , A , B >. ) = ( A i^i ( Cnv3 ` B ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		gdlopcfv8.1	$$⊢\phi \to A\in V$$
2		gdlopcfv8.2	$$⊢\phi \to B\in W$$
3		8olt9o	Could not format 8o e. 9o : No typesetting found for |- 8o e. 9o with typecode |-
4		df-8o	Could not format 8o = suc 7o : No typesetting found for |- 8o = suc 7o with typecode |-
5	3 4	suceldifsn0	Could not format 8o e. ( 9o \ { (/) } ) : No typesetting found for |- 8o e. ( 9o \ { (/) } ) with typecode |-
6	5	a1i	Could not format ( ph -> 8o e. ( 9o \ { (/) } ) ) : No typesetting found for |- ( ph -> 8o e. ( 9o \ { (/) } ) ) with typecode |-
7	1	elexd	$$⊢\phi \to A\in \mathrm{V}$$
8	2	elexd	$$⊢\phi \to B\in \mathrm{V}$$
9		fvexd	Could not format ( ph -> ( ~F8 ` <. A , B >. ) e. _V ) : No typesetting found for |- ( ph -> ( ~F8 ` <. A , B >. ) e. _V ) with typecode |-
10		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
11		8on	Could not format 8o e. On : No typesetting found for |- 8o e. On with typecode |-
12		df-3o	$$⊢3_{𝑜}=\mathrm{suc}{2}_{𝑜}$$
13	10 12	eqsucidi	$$⊢2_{𝑜}\in 3_{𝑜}$$
14		3on	$$⊢3_{𝑜}\in \mathrm{On}$$
15		df-4o	$$⊢4_{𝑜}=\mathrm{suc}{3}_{𝑜}$$
16	14 15	eqsucidi	$$⊢3_{𝑜}\in 4_{𝑜}$$
17		4on	$$⊢4_{𝑜}\in \mathrm{On}$$
18		df-5o	Could not format 5o = suc 4o : No typesetting found for |- 5o = suc 4o with typecode |-
19	17 18	eqsucidi	Could not format 4o e. 5o : No typesetting found for |- 4o e. 5o with typecode |-
20		5on	Could not format 5o e. On : No typesetting found for |- 5o e. On with typecode |-
21		df-6o	Could not format 6o = suc 5o : No typesetting found for |- 6o = suc 5o with typecode |-
22	20 21	eqsucidi	Could not format 5o e. 6o : No typesetting found for |- 5o e. 6o with typecode |-
23		6on	Could not format 6o e. On : No typesetting found for |- 6o e. On with typecode |-
24		df-7o	Could not format 7o = suc 6o : No typesetting found for |- 7o = suc 6o with typecode |-
25	23 24	eqsucidi	Could not format 6o e. 7o : No typesetting found for |- 6o e. 7o with typecode |-
26		7on	Could not format 7o e. On : No typesetting found for |- 7o e. On with typecode |-
27	26 4	eqsucidi	Could not format 7o e. 8o : No typesetting found for |- 7o e. 8o with typecode |-
28	11 25 27	ontr1i	Could not format 6o e. 8o : No typesetting found for |- 6o e. 8o with typecode |-
29	11 22 28	ontr1i	Could not format 5o e. 8o : No typesetting found for |- 5o e. 8o with typecode |-
30	11 19 29	ontr1i	Could not format 4o e. 8o : No typesetting found for |- 4o e. 8o with typecode |-
31	11 16 30	ontr1i	Could not format 3o e. 8o : No typesetting found for |- 3o e. 8o with typecode |-
32	11 13 31	ontr1i	Could not format 2o e. 8o : No typesetting found for |- 2o e. 8o with typecode |-
33	10 11 32	gdlopcfvlem	Could not format ( ( ph /\ 8o = 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 >. ) ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ 8o = 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 >. ) ) ) ) ) ) ) with typecode |-
34		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
35		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
36	34 35	eqsucidi	$$⊢1_{𝑜}\in 2_{𝑜}$$
37	11 36 32	ontr1i	Could not format 1o e. 8o : No typesetting found for |- 1o e. 8o with typecode |-
38	34 11 37	gdlopcfvlem	Could not format ( ( ph /\ 8o = 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 >. ) ) ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ 8o = 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 >. ) ) ) ) ) ) ) ) with typecode |-
39	17 11 30	gdlopcfvlem	Could not format ( ( ph /\ 8o = 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 >. ) ) ) ) ) : No typesetting found for |- ( ( ph /\ 8o = 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 >. ) ) ) ) ) with typecode |-
40	14 11 31	gdlopcfvlem	Could not format ( ( ph /\ 8o = 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 >. ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ 8o = 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 >. ) ) ) ) ) ) with typecode |-
41	20 11 29	gdlopcfvlem	Could not format ( ( ph /\ 8o = 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 >. ) ) ) ) : No typesetting found for |- ( ( ph /\ 8o = 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 >. ) ) ) ) with typecode |-
42	23 11 28	gdlopcfvlem	Could not format ( ( ph /\ 8o = 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 >. ) ) ) : No typesetting found for |- ( ( ph /\ 8o = 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 >. ) ) ) with typecode |-
43	26 11 27	gdlopcfvlem	Could not format ( ( ph /\ 8o = n ) -> if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) = ( ~F8 ` <. x , y >. ) ) : No typesetting found for |- ( ( ph /\ 8o = n ) -> if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) = ( ~F8 ` <. x , y >. ) ) with typecode |-
44	41 42 43	3eqtrrd	Could not format ( ( ph /\ 8o = n ) -> ( ~F8 ` <. x , y >. ) = if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) ) : No typesetting found for |- ( ( ph /\ 8o = n ) -> ( ~F8 ` <. x , y >. ) = if ( n = 5o , ( ~F5 ` <. x , y >. ) , if ( n = 6o , ( ~F6 ` <. x , y >. ) , if ( n = 7o , ( ~F7 ` <. x , y >. ) , ( ~F8 ` <. x , y >. ) ) ) ) ) with typecode |-
45	39 40 44	3eqtr4rd	Could not format ( ( ph /\ 8o = n ) -> ( ~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 >. ) ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ 8o = n ) -> ( ~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 >. ) ) ) ) ) ) ) with typecode |-
46	33 38 45	3eqtr4rd	Could not format ( ( ph /\ 8o = n ) -> ( ~F8 ` <. 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 >. ) ) ) ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ 8o = n ) -> ( ~F8 ` <. 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 >. ) ) ) ) ) ) ) ) ) with typecode |-
47		opeq1	$$⊢A=x\to ⟨A,y⟩=⟨x,y⟩$$
48	47	fveq2d	Could not format ( A = x -> ( ~F8 ` <. A , y >. ) = ( ~F8 ` <. x , y >. ) ) : No typesetting found for |- ( A = x -> ( ~F8 ` <. A , y >. ) = ( ~F8 ` <. x , y >. ) ) with typecode |-
49	48	adantl	Could not format ( ( ph /\ A = x ) -> ( ~F8 ` <. A , y >. ) = ( ~F8 ` <. x , y >. ) ) : No typesetting found for |- ( ( ph /\ A = x ) -> ( ~F8 ` <. A , y >. ) = ( ~F8 ` <. x , y >. ) ) with typecode |-
50		opeq2	$$⊢B=y\to ⟨A,B⟩=⟨A,y⟩$$
51	50	fveq2d	Could not format ( B = y -> ( ~F8 ` <. A , B >. ) = ( ~F8 ` <. A , y >. ) ) : No typesetting found for |- ( B = y -> ( ~F8 ` <. A , B >. ) = ( ~F8 ` <. A , y >. ) ) with typecode |-
52	51	adantl	Could not format ( ( ph /\ B = y ) -> ( ~F8 ` <. A , B >. ) = ( ~F8 ` <. A , y >. ) ) : No typesetting found for |- ( ( ph /\ B = y ) -> ( ~F8 ` <. A , B >. ) = ( ~F8 ` <. A , y >. ) ) with typecode |-
53		df-gdlopc	Could not format ~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 >. ) ) ) ) ) ) ) ) ) : No typesetting found for |- ~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 >. ) ) ) ) ) ) ) ) ) with typecode |-
54	6 7 8 9 46 49 52 53	mpt3fvot2d	Could not format ( ph -> ( ~F ` <. 8o , A , B >. ) = ( ~F8 ` <. A , B >. ) ) : No typesetting found for |- ( ph -> ( ~F ` <. 8o , A , B >. ) = ( ~F8 ` <. A , B >. ) ) with typecode |-
55	1 2	gdlop8fv	Could not format ( ph -> ( ~F8 ` <. A , B >. ) = ( A i^i ( Cnv3 ` B ) ) ) : No typesetting found for |- ( ph -> ( ~F8 ` <. A , B >. ) = ( A i^i ( Cnv3 ` B ) ) ) with typecode |-
56	54 55	eqtrd	Could not format ( ph -> ( ~F ` <. 8o , A , B >. ) = ( A i^i ( Cnv3 ` B ) ) ) : No typesetting found for |- ( ph -> ( ~F ` <. 8o , A , B >. ) = ( A i^i ( Cnv3 ` B ) ) ) with typecode |-