Metamath Proof Explorer

Theorem gonanegoal

Description: The Godel-set for the Sheffer stroke NAND is not equal to the Godel-set of universal quantification. (Contributed by AV, 21-Oct-2023)

Ref Expression
Assertion gonanegoal 
|- ( a |g b ) =/= A.g i u

Proof

Step Hyp Ref Expression
1 1one2o 
 |-  1o =/= 2o
2 1 neii 
 |-  -. 1o = 2o
3 2 intnanr 
 |-  -. ( 1o = 2o /\ <. a , b >. = <. i , u >. )
4 gonafv 
 |-  ( ( a e. _V /\ b e. _V ) -> ( a |g b ) = <. 1o , <. a , b >. >. )
5 4 el2v 
 |-  ( a |g b ) = <. 1o , <. a , b >. >.
6 df-goal 
 |-  A.g i u = <. 2o , <. i , u >. >.
7 5 6 eqeq12i 
 |-  ( ( a |g b ) = A.g i u <-> <. 1o , <. a , b >. >. = <. 2o , <. i , u >. >. )
8 1oex 
 |-  1o e. _V
9 opex 
 |-  <. a , b >. e. _V
10 8 9 opth 
 |-  ( <. 1o , <. a , b >. >. = <. 2o , <. i , u >. >. <-> ( 1o = 2o /\ <. a , b >. = <. i , u >. ) )
11 7 10 bitri 
 |-  ( ( a |g b ) = A.g i u <-> ( 1o = 2o /\ <. a , b >. = <. i , u >. ) )
12 11 necon3abii 
 |-  ( ( a |g b ) =/= A.g i u <-> -. ( 1o = 2o /\ <. a , b >. = <. i , u >. ) )
13 3 12 mpbir 
 |-  ( a |g b ) =/= A.g i u