Theorem gdlop6fv

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

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

Proof

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