Metamath Proof Explorer


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 𝑔 = u V , v V ¬ 𝑔 u 𝑔 v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgoo class 𝑔
1 vu setvar u
2 cvv class V
3 vv setvar v
4 1 cv setvar u
5 4 cgon class ¬ 𝑔 u
6 cgoi class 𝑔
7 3 cv setvar v
8 5 7 6 co class ¬ 𝑔 u 𝑔 v
9 1 3 2 2 8 cmpo class u V , v V ¬ 𝑔 u 𝑔 v
10 0 9 wceq wff 𝑔 = u V , v V ¬ 𝑔 u 𝑔 v