Theorem gdlop4fv

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

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

Proof

Step	Hyp	Ref	Expression
1		gdlop4fv.1	$$⊢\phi \to A\in V$$
2		gdlop4fv.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	1	resexd	$$⊢\phi \to {A\upharpoonright }_B\in \mathrm{V}$$
6		reseq1	$$⊢A=x\to {A\upharpoonright }_y={x\upharpoonright }_y$$
7	6	adantl	$$⊢\left(\phi \wedge A=x\right)\to {A\upharpoonright }_y={x\upharpoonright }_y$$
8		reseq2	$$⊢B=y\to {A\upharpoonright }_B={A\upharpoonright }_y$$
9	8	adantl	$$⊢\left(\phi \wedge B=y\right)\to {A\upharpoonright }_B={A\upharpoonright }_y$$
10		df-gdlop4	Could not format ~F4 = ( x e. _V , y e. _V |-> ( x |` y ) ) : No typesetting found for |- ~F4 = ( x e. _V , y e. _V |-> ( x |` y ) ) with typecode |-
11	3 4 5 7 9 10	mpofvop2d	Could not format ( ph -> ( ~F4 ` <. A , B >. ) = ( A |` B ) ) : No typesetting found for |- ( ph -> ( ~F4 ` <. A , B >. ) = ( A |` B ) ) with typecode |-