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

Metamath Proof Explorer

Definition df-gona

Description: Define the Godel-set for the Sheffer stroke NAND. Here the arguments x = <. U , V >. are also Godel-sets corresponding to smaller formulas. (Contributed by Mario Carneiro, 14-Jul-2013)

Ref Expression
Assertion df-gona ⊼𝑔 = ( 𝑥 ∈ ( V × V ) ↦ ⟨ 1o , 𝑥 ⟩ )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgna ⊢ ⊼𝑔
1 vx ⊢ 𝑥
2 cvv ⊢ V
3 2 2 cxp ⊢ ( V × V )
4 c1o ⊢ 1o
5 1 cv ⊢ 𝑥
6 4 5 cop ⊢ ⟨ 1o , 𝑥 ⟩
7 1 3 6 cmpt ⊢ ( 𝑥 ∈ ( V × V ) ↦ ⟨ 1o , 𝑥 ⟩ )
8 0 7 wceq ⊢ ⊼𝑔 = ( 𝑥 ∈ ( V × V ) ↦ ⟨ 1o , 𝑥 ⟩ )