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 e. Pg <-> ( A e. ( _V X. _V ) /\ ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) )

Proof

Step	Hyp	Ref	Expression
1		elpglem1	|- ( E. x ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) -> ( ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) )
2		elpglem2	|- ( ( ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) -> E. x ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) )
3	1 2	impbii	|- ( E. x ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) <-> ( ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) )
4	3	anbi2i	|- ( ( A e. ( _V X. _V ) /\ E. x ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) ) <-> ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) ) )
5		df-pg	|- Pg = setrecs ( ( y e. _V |-> ( ~P y X. ~P y ) ) )
6	5	elsetrecs	|- ( A e. Pg <-> E. x ( x C_ Pg /\ A e. ( ( y e. _V |-> ( ~P y X. ~P y ) ) ` x ) ) )
7		elpglem3	|- ( E. x ( x C_ Pg /\ A e. ( ( y e. _V |-> ( ~P y X. ~P y ) ) ` x ) ) <-> ( A e. ( _V X. _V ) /\ E. x ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) ) )
8	6 7	bitri	|- ( A e. Pg <-> ( A e. ( _V X. _V ) /\ E. x ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) ) )
9		3anass	|- ( ( A e. ( _V X. _V ) /\ ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) <-> ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) ) )
10	4 8 9	3bitr4i	|- ( A e. Pg <-> ( A e. ( _V X. _V ) /\ ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) )