Theorem gdlop6fv

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

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

Proof

Step	Hyp	Ref	Expression
1		gdlop6fv.1	|- ( ph -> A e. V )
2		gdlop6fv.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 `' B ) e. _V )
6	1 5	syl	|- ( ph -> ( A i^i `' B ) e. _V )
7		ineq1	|- ( A = x -> ( A i^i `' y ) = ( x i^i `' y ) )
8	7	adantl	|- ( ( ph /\ A = x ) -> ( A i^i `' y ) = ( x i^i `' y ) )
9		cnveq	|- ( B = y -> `' B = `' y )
10	9	ineq2d	|- ( B = y -> ( A i^i `' B ) = ( A i^i `' y ) )
11	10	adantl	|- ( ( ph /\ B = y ) -> ( A i^i `' B ) = ( A i^i `' y ) )
12		df-gdlop6	|- ~F6 = ( x e. _V , y e. _V |-> ( x i^i `' y ) )
13	3 4 6 8 11 12	mpofvop2d	|- ( ph -> ( ~F6 ` <. A , B >. ) = ( A i^i `' B ) )