Theorem gdlop2fv

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

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

Proof

Step	Hyp	Ref	Expression
1		gdlop2fv.1	|- ( ph -> A e. V )
2		gdlop2fv.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 _E ) e. _V )
6	1 5	syl	|- ( ph -> ( A i^i _E ) e. _V )
7		ineq1	|- ( A = x -> ( A i^i _E ) = ( x i^i _E ) )
8	7	adantl	|- ( ( ph /\ A = x ) -> ( A i^i _E ) = ( x i^i _E ) )
9		eqidd	|- ( ( ph /\ B = y ) -> ( A i^i _E ) = ( A i^i _E ) )
10		df-gdlop2	|- ~F2 = ( x e. _V , y e. _V |-> ( x i^i _E ) )
11	3 4 6 8 9 10	mpofvop2d	|- ( ph -> ( ~F2 ` <. A , B >. ) = ( A i^i _E ) )