Metamath Proof Explorer

Theorem elpg

Description: Membership in the class of partisan games. In John Horton Conway's On Numbers and Games, this is stated as "If L and R are any two sets of games, then there is a game { L | R } . All games are constructed in this way." The first sentence corresponds to the backward direction of our theorem, and the second to the forward direction. (Contributed by Emmett Weisz, 27-Aug-2021)

Ref Expression
Assertion elpg ⊢ A ∈ Pg ↔ A ∈ V × V ∧ 1 st ⁡ A ⊆ Pg ∧ 2 nd ⁡ A ⊆ Pg

Proof

Step Hyp Ref Expression
1 elpglem1 ⊢ ∃ x x ⊆ Pg ∧ 1 st ⁡ A ∈ 𝒫 x ∧ 2 nd ⁡ A ∈ 𝒫 x → 1 st ⁡ A ⊆ Pg ∧ 2 nd ⁡ A ⊆ Pg
2 elpglem2 ⊢ 1 st ⁡ A ⊆ Pg ∧ 2 nd ⁡ A ⊆ Pg → ∃ x x ⊆ Pg ∧ 1 st ⁡ A ∈ 𝒫 x ∧ 2 nd ⁡ A ∈ 𝒫 x
3 1 2 impbii ⊢ ∃ x x ⊆ Pg ∧ 1 st ⁡ A ∈ 𝒫 x ∧ 2 nd ⁡ A ∈ 𝒫 x ↔ 1 st ⁡ A ⊆ Pg ∧ 2 nd ⁡ A ⊆ Pg
4 3 anbi2i ⊢ A ∈ V × V ∧ ∃ x x ⊆ Pg ∧ 1 st ⁡ A ∈ 𝒫 x ∧ 2 nd ⁡ A ∈ 𝒫 x ↔ A ∈ V × V ∧ 1 st ⁡ A ⊆ Pg ∧ 2 nd ⁡ A ⊆ Pg
5 df-pg ⊢ Pg = setrecs ⁡ y ∈ V ⟼ 𝒫 y × 𝒫 y
6 5 elsetrecs ⊢ A ∈ Pg ↔ ∃ x x ⊆ Pg ∧ A ∈ y ∈ V ⟼ 𝒫 y × 𝒫 y ⁡ x
7 elpglem3 ⊢ ∃ x x ⊆ Pg ∧ A ∈ y ∈ V ⟼ 𝒫 y × 𝒫 y ⁡ x ↔ A ∈ V × V ∧ ∃ x x ⊆ Pg ∧ 1 st ⁡ A ∈ 𝒫 x ∧ 2 nd ⁡ A ∈ 𝒫 x
8 6 7 bitri ⊢ A ∈ Pg ↔ A ∈ V × V ∧ ∃ x x ⊆ Pg ∧ 1 st ⁡ A ∈ 𝒫 x ∧ 2 nd ⁡ A ∈ 𝒫 x
9 3anass ⊢ A ∈ V × V ∧ 1 st ⁡ A ⊆ Pg ∧ 2 nd ⁡ A ⊆ Pg ↔ A ∈ V × V ∧ 1 st ⁡ A ⊆ Pg ∧ 2 nd ⁡ A ⊆ Pg
10 4 8 9 3bitr4i ⊢ A ∈ Pg ↔ A ∈ V × V ∧ 1 st ⁡ A ⊆ Pg ∧ 2 nd ⁡ A ⊆ Pg