Definition df-pg 42781

Description: Define the class of partizan games. More precisely, this is the class of partizan game forms, many of which represent equal partisan games. In metamath, equality between partizan 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 42780	. 2 class Pg
2		vx	. . . 4 setvar 𝑥
3		cvv 3231	. . . 4 class V
4	2	cv 1522	. . . . . 6 class 𝑥
5	4	cpw 4191	. . . . 5 class 𝒫 𝑥
6	5, 5	cxp 5141	. . . 4 class (𝒫 𝑥 × 𝒫 𝑥)
7	2, 3, 6	cmpt 4762	. . 3 class (𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥))
8	7	csetrecs 42755	. 2 class setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥)))
9	1, 8	wceq 1523	1 wff Pg = setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥)))

This definition is referenced by:  elpg  42785