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	⊢ ( 𝐴 ∈ Pg ↔ ( 𝐴 ∈ ( V × V ) ∧ ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) )

Proof

Step	Hyp	Ref	Expression
1		elpglem1	⊢ ( ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) → ( ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) )
2		elpglem2	⊢ ( ( ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) → ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) )
3	1 2	impbii	⊢ ( ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) ↔ ( ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) )
4	3	anbi2i	⊢ ( ( 𝐴 ∈ ( V × V ) ∧ ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) ) )
5		df-pg	⊢ Pg = setrecs ( ( 𝑦 ∈ V ↦ ( 𝒫 𝑦 × 𝒫 𝑦 ) ) )
6	5	elsetrecs	⊢ ( 𝐴 ∈ Pg ↔ ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ 𝐴 ∈ ( ( 𝑦 ∈ V ↦ ( 𝒫 𝑦 × 𝒫 𝑦 ) ) ‘ 𝑥 ) ) )
7		elpglem3	⊢ ( ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ 𝐴 ∈ ( ( 𝑦 ∈ V ↦ ( 𝒫 𝑦 × 𝒫 𝑦 ) ) ‘ 𝑥 ) ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) ) )
8	6 7	bitri	⊢ ( 𝐴 ∈ Pg ↔ ( 𝐴 ∈ ( V × V ) ∧ ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) ) )
9		3anass	⊢ ( ( 𝐴 ∈ ( V × V ) ∧ ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) ) )
10	4 8 9	3bitr4i	⊢ ( 𝐴 ∈ Pg ↔ ( 𝐴 ∈ ( V × V ) ∧ ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) )

Metamath Proof Explorer

Theorem elpg

Proof