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 48941
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
StepHypRef Expression
1 cpg 48940 . 2 class Pg
2 vx . . . 4 setvar 𝑥
3 cvv 3478 . . . 4 class V
42cv 1536 . . . . . 6 class 𝑥
54cpw 4605 . . . . 5 class 𝒫 𝑥
65, 5cxp 5687 . . . 4 class (𝒫 𝑥 × 𝒫 𝑥)
72, 3, 6cmpt 5231 . . 3 class (𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥))
87csetrecs 48914 . 2 class setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥)))
91, 8wceq 1537 1 wff Pg = setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥)))
Colors of variables: wff setvar class
This definition is referenced by:  elpg  48945  pgindnf  48947
  Copyright terms: Public domain W3C validator