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	eqtrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ⊼𝑔 𝐵 ) = ⟨ 1o , ⟨ 𝐴 , 𝐵 ⟩ ⟩ )