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	$$⊢\left(A\in V\wedge B\in W\right)\to A{⊼}_{𝑔}B=⟨1_{𝑜},⟨A,B⟩⟩$$

Proof

Step	Hyp	Ref	Expression
1		df-ov	$$⊢A{⊼}_{𝑔}B={⊼}_{𝑔}\left(⟨A,B⟩\right)$$
2		opelvvg	$$⊢\left(A\in V\wedge B\in W\right)\to ⟨A,B⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
3		opeq2	$$⊢x=⟨A,B⟩\to ⟨1_{𝑜},x⟩=⟨1_{𝑜},⟨A,B⟩⟩$$
4		df-gona	$$⊢{⊼}_{𝑔}=\left(x\in \left(\mathrm{V}\times \mathrm{V}\right)⟼⟨1_{𝑜},x⟩\right)$$
5		opex	$$⊢⟨1_{𝑜},⟨A,B⟩⟩\in \mathrm{V}$$
6	3 4 5	fvmpt	$$⊢⟨A,B⟩\in \left(\mathrm{V}\times \mathrm{V}\right)\to {⊼}_{𝑔}\left(⟨A,B⟩\right)=⟨1_{𝑜},⟨A,B⟩⟩$$
7	2 6	syl	$$⊢\left(A\in V\wedge B\in W\right)\to {⊼}_{𝑔}\left(⟨A,B⟩\right)=⟨1_{𝑜},⟨A,B⟩⟩$$
8	1 7	syl5eq	$$⊢\left(A\in V\wedge B\in W\right)\to A{⊼}_{𝑔}B=⟨1_{𝑜},⟨A,B⟩⟩$$