Users' Mathboxes Mathbox for Emmett Weisz < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-pg Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 cpg 42780 . 2 class Pg
2 vx . . . 4 setvar 𝑥
3 cvv 3231 . . . 4 class V
42cv 1522 . . . . . 6 class 𝑥
54cpw 4191 . . . . 5 class 𝒫 𝑥
65, 5cxp 5141 . . . 4 class (𝒫 𝑥 × 𝒫 𝑥)
72, 3, 6cmpt 4762 . . 3 class (𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥))
87csetrecs 42755 . 2 class setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥)))
91, 8wceq 1523 1 wff Pg = setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥)))
Colors of variables: wff setvar class
This definition is referenced by:  elpg  42785
  Copyright terms: Public domain W3C validator