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	$$⊢\phi \to A\in V$$
	gdlopcfv1.2	$$⊢\phi \to B\in W$$
Assertion	gdlopcfv1	Could not format assertion : No typesetting found for |- ( ph -> ( ~F ` <. 1o , A , B >. ) = { A , B } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		gdlopcfv1.1	$$⊢\phi \to A\in V$$
2		gdlopcfv1.2	$$⊢\phi \to B\in W$$
3		1olt9o	Could not format 1o e. 9o : No typesetting found for |- 1o e. 9o with typecode |-
4		df-1o	$$⊢1_{𝑜}=\mathrm{suc}\varnothing$$
5	3 4	suceldifsn0	Could not format 1o e. ( 9o \ { (/) } ) : No typesetting found for |- 1o e. ( 9o \ { (/) } ) with typecode |-
6	5	a1i	Could not format ( ph -> 1o e. ( 9o \ { (/) } ) ) : No typesetting found for |- ( ph -> 1o 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 -> ( ~F1 ` <. A , B >. ) e. _V ) : No typesetting found for |- ( ph -> ( ~F1 ` <. A , B >. ) e. _V ) with typecode |-
10		eqcom	$$⊢1_{𝑜}=n\leftrightarrow n=1_{𝑜}$$
11	10	bilani	$$⊢\left(\phi \wedge 1_{𝑜}=n\right)\to n=1_{𝑜}$$
12	11	iftrued	Could not format ( ( 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 >. ) ) : No typesetting found for |- ( ( 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 >. ) ) with typecode |-
13	12	eqcomd	Could not format ( ( 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 >. ) ) ) ) ) ) ) ) ) : No typesetting found for |- ( ( 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 >. ) ) ) ) ) ) ) ) ) with typecode |-
14		opeq1	$$⊢A=x\to ⟨A,y⟩=⟨x,y⟩$$
15	14	fveq2d	Could not format ( A = x -> ( ~F1 ` <. A , y >. ) = ( ~F1 ` <. x , y >. ) ) : No typesetting found for |- ( A = x -> ( ~F1 ` <. A , y >. ) = ( ~F1 ` <. x , y >. ) ) with typecode |-
16	15	adantl	Could not format ( ( ph /\ A = x ) -> ( ~F1 ` <. A , y >. ) = ( ~F1 ` <. x , y >. ) ) : No typesetting found for |- ( ( ph /\ A = x ) -> ( ~F1 ` <. A , y >. ) = ( ~F1 ` <. x , y >. ) ) with typecode |-
17		opeq2	$$⊢B=y\to ⟨A,B⟩=⟨A,y⟩$$
18	17	fveq2d	Could not format ( B = y -> ( ~F1 ` <. A , B >. ) = ( ~F1 ` <. A , y >. ) ) : No typesetting found for |- ( B = y -> ( ~F1 ` <. A , B >. ) = ( ~F1 ` <. A , y >. ) ) with typecode |-
19	18	adantl	Could not format ( ( ph /\ B = y ) -> ( ~F1 ` <. A , B >. ) = ( ~F1 ` <. A , y >. ) ) : No typesetting found for |- ( ( ph /\ B = y ) -> ( ~F1 ` <. A , B >. ) = ( ~F1 ` <. A , y >. ) ) with typecode |-
20		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 |-
21	6 7 8 9 13 16 19 20	mpt3fvot2d	Could not format ( ph -> ( ~F ` <. 1o , A , B >. ) = ( ~F1 ` <. A , B >. ) ) : No typesetting found for |- ( ph -> ( ~F ` <. 1o , A , B >. ) = ( ~F1 ` <. A , B >. ) ) with typecode |-
22	1 2	gdlop1fv	Could not format ( ph -> ( ~F1 ` <. A , B >. ) = { A , B } ) : No typesetting found for |- ( ph -> ( ~F1 ` <. A , B >. ) = { A , B } ) with typecode |-
23	21 22	eqtrd	Could not format ( ph -> ( ~F ` <. 1o , A , B >. ) = { A , B } ) : No typesetting found for |- ( ph -> ( ~F ` <. 1o , A , B >. ) = { A , B } ) with typecode |-