Theorem gdlop8fv

Description: The value of the eighth Gödel operation. (Contributed by BTernaryTau, 18-Oct-2026)

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

Proof

Step	Hyp	Ref	Expression
1		gdlop8fv.1	$$⊢\phi \to A\in V$$
2		gdlop8fv.2	$$⊢\phi \to B\in W$$
3	1	elexd	$$⊢\phi \to A\in \mathrm{V}$$
4	2	elexd	$$⊢\phi \to B\in \mathrm{V}$$
5		inex1g	Could not format ( A e. V -> ( A i^i ( Cnv3 ` B ) ) e. _V ) : No typesetting found for |- ( A e. V -> ( A i^i ( Cnv3 ` B ) ) e. _V ) with typecode |-
6	1 5	syl	Could not format ( ph -> ( A i^i ( Cnv3 ` B ) ) e. _V ) : No typesetting found for |- ( ph -> ( A i^i ( Cnv3 ` B ) ) e. _V ) with typecode |-
7		ineq1	Could not format ( A = x -> ( A i^i ( Cnv3 ` y ) ) = ( x i^i ( Cnv3 ` y ) ) ) : No typesetting found for |- ( A = x -> ( A i^i ( Cnv3 ` y ) ) = ( x i^i ( Cnv3 ` y ) ) ) with typecode |-
8	7	adantl	Could not format ( ( ph /\ A = x ) -> ( A i^i ( Cnv3 ` y ) ) = ( x i^i ( Cnv3 ` y ) ) ) : No typesetting found for |- ( ( ph /\ A = x ) -> ( A i^i ( Cnv3 ` y ) ) = ( x i^i ( Cnv3 ` y ) ) ) with typecode |-
9		fveq2	Could not format ( B = y -> ( Cnv3 ` B ) = ( Cnv3 ` y ) ) : No typesetting found for |- ( B = y -> ( Cnv3 ` B ) = ( Cnv3 ` y ) ) with typecode |-
10	9	ineq2d	Could not format ( B = y -> ( A i^i ( Cnv3 ` B ) ) = ( A i^i ( Cnv3 ` y ) ) ) : No typesetting found for |- ( B = y -> ( A i^i ( Cnv3 ` B ) ) = ( A i^i ( Cnv3 ` y ) ) ) with typecode |-
11	10	adantl	Could not format ( ( ph /\ B = y ) -> ( A i^i ( Cnv3 ` B ) ) = ( A i^i ( Cnv3 ` y ) ) ) : No typesetting found for |- ( ( ph /\ B = y ) -> ( A i^i ( Cnv3 ` B ) ) = ( A i^i ( Cnv3 ` y ) ) ) with typecode |-
12		df-gdlop8	Could not format ~F8 = ( x e. _V , y e. _V |-> ( x i^i ( Cnv3 ` y ) ) ) : No typesetting found for |- ~F8 = ( x e. _V , y e. _V |-> ( x i^i ( Cnv3 ` y ) ) ) with typecode |-
13	3 4 6 8 11 12	mpofvop2d	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 |-