Theorem gdlop5fv

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

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

Proof

Step	Hyp	Ref	Expression
1		gdlop5fv.1	$$⊢\phi \to A\in V$$
2		gdlop5fv.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	$$⊢A\in V\to A\cap \mathrm{dom}B\in \mathrm{V}$$
6	1 5	syl	$$⊢\phi \to A\cap \mathrm{dom}B\in \mathrm{V}$$
7		ineq1	$$⊢A=x\to A\cap \mathrm{dom}y=x\cap \mathrm{dom}y$$
8	7	adantl	$$⊢\left(\phi \wedge A=x\right)\to A\cap \mathrm{dom}y=x\cap \mathrm{dom}y$$
9		dmeq	$$⊢B=y\to \mathrm{dom}B=\mathrm{dom}y$$
10	9	ineq2d	$$⊢B=y\to A\cap \mathrm{dom}B=A\cap \mathrm{dom}y$$
11	10	adantl	$$⊢\left(\phi \wedge B=y\right)\to A\cap \mathrm{dom}B=A\cap \mathrm{dom}y$$
12		df-gdlop5	Could not format ~F5 = ( x e. _V , y e. _V |-> ( x i^i dom y ) ) : No typesetting found for |- ~F5 = ( x e. _V , y e. _V |-> ( x i^i dom y ) ) with typecode |-
13	3 4 6 8 11 12	mpofvop2d	Could not format ( ph -> ( ~F5 ` <. A , B >. ) = ( A i^i dom B ) ) : No typesetting found for |- ( ph -> ( ~F5 ` <. A , B >. ) = ( A i^i dom B ) ) with typecode |-