Definition df-goor

Description: Define the Godel-set of disjunction. Here the arguments U and V are also Godel-sets corresponding to smaller formulas. Note that this is aclass expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013)

	Ref	Expression
Assertion	df-goor	⊢ ∨𝑔 = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( ¬𝑔 𝑢 →𝑔 𝑣 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgoo	⊢ ∨𝑔
1		vu	⊢ 𝑢
2		cvv	⊢ V
3		vv	⊢ 𝑣
4	1	cv	⊢ 𝑢
5	4	cgon	⊢ ¬𝑔 𝑢
6		cgoi	⊢ →𝑔
7	3	cv	⊢ 𝑣
8	5 7 6	co	⊢ ( ¬𝑔 𝑢 →𝑔 𝑣 )
9	1 3 2 2 8	cmpo	⊢ ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( ¬𝑔 𝑢 →𝑔 𝑣 ) )
10	0 9	wceq	⊢ ∨𝑔 = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( ¬𝑔 𝑢 →𝑔 𝑣 ) )