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

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

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