Theorem gdlop4fv

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

	Ref	Expression
Hypotheses	gdlop4fv.1	|- ( ph -> A e. V )
	gdlop4fv.2	|- ( ph -> B e. W )
Assertion	gdlop4fv	|- ( ph -> ( ~F4 ` <. A , B >. ) = ( A |` B ) )

Proof

Step	Hyp	Ref	Expression
1		gdlop4fv.1	|- ( ph -> A e. V )
2		gdlop4fv.2	|- ( ph -> B e. W )
3	1	elexd	|- ( ph -> A e. _V )
4	2	elexd	|- ( ph -> B e. _V )
5	1	resexd	|- ( ph -> ( A |` B ) e. _V )
6		reseq1	|- ( A = x -> ( A |` y ) = ( x |` y ) )
7	6	adantl	|- ( ( ph /\ A = x ) -> ( A |` y ) = ( x |` y ) )
8		reseq2	|- ( B = y -> ( A |` B ) = ( A |` y ) )
9	8	adantl	|- ( ( ph /\ B = y ) -> ( A |` B ) = ( A |` y ) )
10		df-gdlop4	|- ~F4 = ( x e. _V , y e. _V |-> ( x |` y ) )
11	3 4 5 7 9 10	mpofvop2d	|- ( ph -> ( ~F4 ` <. A , B >. ) = ( A |` B ) )