Definition df-pg 47755

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 47754	. 2 class Pg
2		vx	. . . 4 setvar 𝑥
3		cvv 3475	. . . 4 class V
4	2	cv 1541	. . . . . 6 class 𝑥
5	4	cpw 4603	. . . . 5 class 𝒫 𝑥
6	5, 5	cxp 5675	. . . 4 class (𝒫 𝑥 × 𝒫 𝑥)
7	2, 3, 6	cmpt 5232	. . 3 class (𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥))
8	7	csetrecs 47728	. 2 class setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥)))
9	1, 8	wceq 1542	1 wff Pg = setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥)))

This definition is referenced by:  elpg  47759  pgindnf  47761