Metamath Proof Explorer


Theorem gonafv

Description: The "Godel-set for the Sheffer stroke NAND" for two formulas A and B . (Contributed by AV, 16-Oct-2023)

Ref Expression
Assertion gonafv ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴𝑔 𝐵 ) = ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ )

Proof

Step Hyp Ref Expression
1 df-ov ( 𝐴𝑔 𝐵 ) = ( ⊼𝑔 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
2 opelvvg ( ( 𝐴𝑉𝐵𝑊 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) )
3 opeq2 ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ⟨ 1o , 𝑥 ⟩ = ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ )
4 df-gona 𝑔 = ( 𝑥 ∈ ( V × V ) ↦ ⟨ 1o , 𝑥 ⟩ )
5 opex ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ ∈ V
6 3 4 5 fvmpt ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) → ( ⊼𝑔 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ )
7 2 6 syl ( ( 𝐴𝑉𝐵𝑊 ) → ( ⊼𝑔 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ )
8 1 7 syl5eq ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴𝑔 𝐵 ) = ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ )