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{⊼}_{𝑔}b\ne \left[{\forall }_{𝑔}iu\right]$$

Proof

Step	Hyp	Ref	Expression
1		1one2o	$$⊢1_{𝑜}\ne 2_{𝑜}$$
2	1	neii	$$⊢\neg 1_{𝑜}=2_{𝑜}$$
3	2	intnanr	$$⊢\neg \left(1_{𝑜}=2_{𝑜}\wedge ⟨a,b⟩=⟨i,u⟩\right)$$
4		gonafv	$$⊢\left(a\in \mathrm{V}\wedge b\in \mathrm{V}\right)\to a{⊼}_{𝑔}b=⟨1_{𝑜},⟨a,b⟩⟩$$
5	4	el2v	$$⊢a{⊼}_{𝑔}b=⟨1_{𝑜},⟨a,b⟩⟩$$
6		df-goal	$$⊢\left[{\forall }_{𝑔}iu\right]=⟨2_{𝑜},⟨i,u⟩⟩$$
7	5 6	eqeq12i	$$⊢a{⊼}_{𝑔}b=\left[{\forall }_{𝑔}iu\right]\leftrightarrow ⟨1_{𝑜},⟨a,b⟩⟩=⟨2_{𝑜},⟨i,u⟩⟩$$
8		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
9		opex	$$⊢⟨a,b⟩\in \mathrm{V}$$
10	8 9	opth	$$⊢⟨1_{𝑜},⟨a,b⟩⟩=⟨2_{𝑜},⟨i,u⟩⟩\leftrightarrow \left(1_{𝑜}=2_{𝑜}\wedge ⟨a,b⟩=⟨i,u⟩\right)$$
11	7 10	bitri	$$⊢a{⊼}_{𝑔}b=\left[{\forall }_{𝑔}iu\right]\leftrightarrow \left(1_{𝑜}=2_{𝑜}\wedge ⟨a,b⟩=⟨i,u⟩\right)$$
12	11	necon3abii	$$⊢a{⊼}_{𝑔}b\ne \left[{\forall }_{𝑔}iu\right]\leftrightarrow \neg \left(1_{𝑜}=2_{𝑜}\wedge ⟨a,b⟩=⟨i,u⟩\right)$$
13	3 12	mpbir	$$⊢a{⊼}_{𝑔}b\ne \left[{\forall }_{𝑔}iu\right]$$