Mathbox for Emmett Weisz |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-pg | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-pg | ⊢ Pg = setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cpg 42251 | . 2 class Pg | |
2 | vx | . . . 4 setvar 𝑥 | |
3 | cvv 3173 | . . . 4 class V | |
4 | 2 | cv 1474 | . . . . . 6 class 𝑥 |
5 | 4 | cpw 4108 | . . . . 5 class 𝒫 𝑥 |
6 | 5, 5 | cxp 5036 | . . . 4 class (𝒫 𝑥 × 𝒫 𝑥) |
7 | 2, 3, 6 | cmpt 4643 | . . 3 class (𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥)) |
8 | 7 | csetrecs 42229 | . 2 class setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥))) |
9 | 1, 8 | wceq 1475 | 1 wff Pg = setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥))) |
Colors of variables: wff setvar class |
This definition is referenced by: elpg 42256 |
Copyright terms: Public domain | W3C validator |