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	⊢ ( 𝑎 ⊼𝑔 𝑏 ) ≠ ∀𝑔 𝑖 𝑢

Proof

Step	Hyp	Ref	Expression
1		1one2o	⊢ 1o ≠ 2o
2	1	neii	⊢ ¬ 1o = 2o
3	2	intnanr	⊢ ¬ ( 1o = 2o ∧ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑖 , 𝑢 ⟩ )
4		gonafv	⊢ ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) → ( 𝑎 ⊼𝑔 𝑏 ) = ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ )
5	4	el2v	⊢ ( 𝑎 ⊼𝑔 𝑏 ) = ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩
6		df-goal	⊢ ∀𝑔 𝑖 𝑢 = ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩
7	5 6	eqeq12i	⊢ ( ( 𝑎 ⊼𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 ↔ ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩ )
8		1oex	⊢ 1o ∈ V
9		opex	⊢ ⟨ 𝑎 , 𝑏 ⟩ ∈ V
10	8 9	opth	⊢ ( ⟨ 1o , ⟨ 𝑎 , 𝑏 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩ ↔ ( 1o = 2o ∧ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑖 , 𝑢 ⟩ ) )
11	7 10	bitri	⊢ ( ( 𝑎 ⊼𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 ↔ ( 1o = 2o ∧ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑖 , 𝑢 ⟩ ) )
12	11	necon3abii	⊢ ( ( 𝑎 ⊼𝑔 𝑏 ) ≠ ∀𝑔 𝑖 𝑢 ↔ ¬ ( 1o = 2o ∧ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑖 , 𝑢 ⟩ ) )
13	3 12	mpbir	⊢ ( 𝑎 ⊼𝑔 𝑏 ) ≠ ∀𝑔 𝑖 𝑢