Metamath Proof Explorer


Definition df-pg

Description: Define the class of partisan games. More precisely, this is the class of partisan game forms, many of which represent equal partisan games. In Metamath, equality between partisan games is represented by a different equivalence relation than class equality. (Contributed by Emmett Weisz, 22-Aug-2021)

Ref Expression
Assertion df-pg Pg = setrecs x V 𝒫 x × 𝒫 x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpg class Pg
1 vx setvar x
2 cvv class V
3 1 cv setvar x
4 3 cpw class 𝒫 x
5 4 4 cxp class 𝒫 x × 𝒫 x
6 1 2 5 cmpt class x V 𝒫 x × 𝒫 x
7 6 csetrecs class setrecs x V 𝒫 x × 𝒫 x
8 0 7 wceq wff Pg = setrecs x V 𝒫 x × 𝒫 x