Theorem gonafv

Description: The "Godel-set for the Sheffer stroke NAND" for two formulas A and B . (Contributed by AV, 16-Oct-2023)

	Ref	Expression
Assertion	gonafv	|- ( ( A e. V /\ B e. W ) -> ( A |g B ) = <. 1o , <. A , B >. >. )

Proof

Step	Hyp	Ref	Expression
1		df-ov	|- ( A |g B ) = ( |g ` <. A , B >. )
2		opelvvg	|- ( ( A e. V /\ B e. W ) -> <. A , B >. e. ( _V X. _V ) )
3		opeq2	|- ( x = <. A , B >. -> <. 1o , x >. = <. 1o , <. A , B >. >. )
4		df-gona	|- |g = ( x e. ( _V X. _V ) |-> <. 1o , x >. )
5		opex	|- <. 1o , <. A , B >. >. e. _V
6	3 4 5	fvmpt	|- ( <. A , B >. e. ( _V X. _V ) -> ( |g ` <. A , B >. ) = <. 1o , <. A , B >. >. )
7	2 6	syl	|- ( ( A e. V /\ B e. W ) -> ( |g ` <. A , B >. ) = <. 1o , <. A , B >. >. )
8	1 7	syl5eq	|- ( ( A e. V /\ B e. W ) -> ( A |g B ) = <. 1o , <. A , B >. >. )