This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( ( A e. V /\ B e. W ) -> ( A |g B ) = <. 1o , <. A , B >. >. )