Theorem gdlop7fv

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

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

Proof

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