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 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.) |
Ref | Expression |
---|---|
df-pg | ⊢ Pg = setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cpg 44739 | . 2 class Pg | |
2 | vx | . . . 4 setvar 𝑥 | |
3 | cvv 3492 | . . . 4 class V | |
4 | 2 | cv 1527 | . . . . . 6 class 𝑥 |
5 | 4 | cpw 4535 | . . . . 5 class 𝒫 𝑥 |
6 | 5, 5 | cxp 5546 | . . . 4 class (𝒫 𝑥 × 𝒫 𝑥) |
7 | 2, 3, 6 | cmpt 5137 | . . 3 class (𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥)) |
8 | 7 | csetrecs 44714 | . 2 class setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥))) |
9 | 1, 8 | wceq 1528 | 1 wff Pg = setrecs((𝑥 ∈ V ↦ (𝒫 𝑥 × 𝒫 𝑥))) |
Colors of variables: wff setvar class |
This definition is referenced by: elpg 44744 |
Copyright terms: Public domain | W3C validator |