Definition df-pg 48802

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 48801	. 2 class Pg
2		vx	. . . 4 setvar 𝑥
3		cvv 3488	. . . 4 class V
4	2	cv 1536	. . . . . 6 class 𝑥
5	4	cpw 4622	. . . . 5 class 𝒫 𝑥
6	5, 5	cxp 5698	. . . 4 class (𝒫 𝑥 × 𝒫 𝑥)
7	2, 3, 6	cmpt 5249	. . 3 class (𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥))
8	7	csetrecs 48775	. 2 class setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥)))
9	1, 8	wceq 1537	1 wff Pg = setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥)))

This definition is referenced by:  elpg  48806  pgindnf  48808