Definition df-pg 51209

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.)

Assertion

Ref	Expression
df-pg	⊢ Pg = setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥)))

Detailed syntax breakdown of Definition df-pg

Step	Hyp	Ref	Expression
1		cpg 51208	. 2 class Pg
2		vx	. . . 4 setvar 𝑥
3		cvv 3454	. . . 4 class V
4	2	cv 1569	. . . . . 6 class 𝑥
5	4	cpw 4560	. . . . 5 class 𝒫 𝑥
6	5, 5	cxp 5656	. . . 4 class (𝒫 𝑥 × 𝒫 𝑥)
7	2, 3, 6	cmpt 5192	. . 3 class (𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥))
8	7	csetrecs 10001	. 2 class setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥)))
9	1, 8	wceq 1570	1 wff Pg = setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥)))

This definition is used by:  elpg  51213  pgindnf  51215