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

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	⊢ ∧_𝑔 = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ¬_𝑔 ( 𝑢 ⊼_𝑔 𝑣 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgoa	⊢ ∧_𝑔
1		vu	⊢ 𝑢
2		cvv	⊢ V
3		vv	⊢ 𝑣
4	1	cv	⊢ 𝑢
5		cgna	⊢ ⊼_𝑔
6	3	cv	⊢ 𝑣
7	4 6 5	co	⊢ ( 𝑢 ⊼_𝑔 𝑣 )
8	7	cgon	⊢ ¬_𝑔 ( 𝑢 ⊼_𝑔 𝑣 )
9	1 3 2 2 8	cmpo	⊢ ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ¬_𝑔 ( 𝑢 ⊼_𝑔 𝑣 ) )
10	0 9	wceq	⊢ ∧_𝑔 = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ¬_𝑔 ( 𝑢 ⊼_𝑔 𝑣 ) )