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 \in Pg \leftrightarrow (A \in (V \times V) \land 1^{st} (A) \subseteq Pg \land 2^{nd} (A) \subseteq Pg)$

Proof

Step	Hyp	Ref	Expression
1		elpglem1	$⊢ \exists x (x \subseteq Pg \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x)) \to (1^{st} (A) \subseteq Pg \land 2^{nd} (A) \subseteq Pg)$
2		elpglem2	$⊢ (1^{st} (A) \subseteq Pg \land 2^{nd} (A) \subseteq Pg) \to \exists x (x \subseteq Pg \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x))$
3	1 2	impbii	$⊢ \exists x (x \subseteq Pg \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x)) \leftrightarrow (1^{st} (A) \subseteq Pg \land 2^{nd} (A) \subseteq Pg)$
4	3	anbi2i	$⊢ (A \in (V \times V) \land \exists x (x \subseteq Pg \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x))) \leftrightarrow (A \in (V \times V) \land (1^{st} (A) \subseteq Pg \land 2^{nd} (A) \subseteq Pg))$
5		df-pg	$⊢ Pg = setrecs ((y \in V ⟼ 𝒫 y \times 𝒫 y))$
6	5	elsetrecs	$⊢ A \in Pg \leftrightarrow \exists x (x \subseteq Pg \land A \in (y \in V ⟼ 𝒫 y \times 𝒫 y) (x))$
7		elpglem3	$⊢ \exists x (x \subseteq Pg \land A \in (y \in V ⟼ 𝒫 y \times 𝒫 y) (x)) \leftrightarrow (A \in (V \times V) \land \exists x (x \subseteq Pg \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x)))$
8	6 7	bitri	$⊢ A \in Pg \leftrightarrow (A \in (V \times V) \land \exists x (x \subseteq Pg \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x)))$
9		3anass	$⊢ (A \in (V \times V) \land 1^{st} (A) \subseteq Pg \land 2^{nd} (A) \subseteq Pg) \leftrightarrow (A \in (V \times V) \land (1^{st} (A) \subseteq Pg \land 2^{nd} (A) \subseteq Pg))$
10	4 8 9	3bitr4i	$⊢ A \in Pg \leftrightarrow (A \in (V \times V) \land 1^{st} (A) \subseteq Pg \land 2^{nd} (A) \subseteq Pg)$

Metamath Proof Explorer

Theorem elpg

Proof