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