Theorem gdlop7fv

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

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

Proof

Step	Hyp	Ref	Expression
1		gdlop7fv.1	|- ( ph -> A e. V )
2		gdlop7fv.2	|- ( ph -> B e. W )
3	1	elexd	|- ( ph -> A e. _V )
4	2	elexd	|- ( ph -> B e. _V )
5		inex1g	|- ( A e. V -> ( A i^i ( Cnv2 ` B ) ) e. _V )
6	1 5	syl	|- ( ph -> ( A i^i ( Cnv2 ` B ) ) e. _V )
7		ineq1	|- ( A = x -> ( A i^i ( Cnv2 ` y ) ) = ( x i^i ( Cnv2 ` y ) ) )
8	7	adantl	|- ( ( ph /\ A = x ) -> ( A i^i ( Cnv2 ` y ) ) = ( x i^i ( Cnv2 ` y ) ) )
9		fveq2	|- ( B = y -> ( Cnv2 ` B ) = ( Cnv2 ` y ) )
10	9	ineq2d	|- ( B = y -> ( A i^i ( Cnv2 ` B ) ) = ( A i^i ( Cnv2 ` y ) ) )
11	10	adantl	|- ( ( ph /\ B = y ) -> ( A i^i ( Cnv2 ` B ) ) = ( A i^i ( Cnv2 ` y ) ) )
12		df-gdlop7	|- ~F7 = ( x e. _V , y e. _V |-> ( x i^i ( Cnv2 ` y ) ) )
13	3 4 6 8 11 12	mpofvop2d	|- ( ph -> ( ~F7 ` <. A , B >. ) = ( A i^i ( Cnv2 ` B ) ) )