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 ⊼_{𝑔} b \neq [\forall_{𝑔} i u]$

Proof

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