Metamath Proof Explorer

Definition df-goan

Description: Define the Godel-set of conjunction. Here the arguments U and V are also Godel-sets corresponding to smaller formulas. (Contributed by Mario Carneiro, 14-Jul-2013)

		Ref	Expression
	Assertion	df-goan	$⊢ \land_{𝑔} = (u \in V, v \in V ⟼ [\neg_{𝑔} (u ⊼_{𝑔} v)])$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgoa	$class \land_{𝑔}$
1		vu	$setvar u$
2		cvv	$class V$
3		vv	$setvar v$
4	1	cv	$setvar u$
5		cgna	$class ⊼_{𝑔}$
6	3	cv	$setvar v$
7	4 6 5	co	$class (u ⊼_{𝑔} v)$
8	7	cgon	$class [\neg_{𝑔} (u ⊼_{𝑔} v)]$
9	1 3 2 2 8	cmpo	$class (u \in V, v \in V ⟼ [\neg_{𝑔} (u ⊼_{𝑔} v)])$
10	0 9	wceq	$wff \land_{𝑔} = (u \in V, v \in V ⟼ [\neg_{𝑔} (u ⊼_{𝑔} v)])$