Theorem pgind

Description: Induction on partizan games. (Contributed by Emmett Weisz, 27-May-2024)

	Ref	Expression
Hypotheses	pgind.1	|- ( x = y -> ( ps <-> ch ) )
	pgind.2	|- ( y = A -> ( ch <-> th ) )
	pgind.3	|- ( ph -> A. x ( A. y e. ( ( 1st ` x ) u. ( 2nd ` x ) ) ch -> ps ) )
Assertion	pgind	|- ( ph -> ( A e. Pg -> th ) )

Proof

Step	Hyp	Ref	Expression
1		pgind.1	|- ( x = y -> ( ps <-> ch ) )
2		pgind.2	|- ( y = A -> ( ch <-> th ) )
3		pgind.3	|- ( ph -> A. x ( A. y e. ( ( 1st ` x ) u. ( 2nd ` x ) ) ch -> ps ) )
4		19.8a	|- ( ph -> E. y ph )
5		19.8a	|- ( E. y ph -> E. x E. y ph )
6		nfe1	|- F/ x E. x E. y ph
7		nfe1	|- F/ y E. y ph
8	7	nfex	|- F/ y E. x E. y ph
9		nfa1	|- F/ x A. x ( A. y e. ( ( 1st ` x ) u. ( 2nd ` x ) ) ch -> ps )
10		nfra1	|- F/ y A. y e. ( ( 1st ` x ) u. ( 2nd ` x ) ) ch
11		nfv	|- F/ y ps
12	10 11	nfim	|- F/ y ( A. y e. ( ( 1st ` x ) u. ( 2nd ` x ) ) ch -> ps )
13	12	nfal	|- F/ y A. x ( A. y e. ( ( 1st ` x ) u. ( 2nd ` x ) ) ch -> ps )
14	13 3	exlimi	|- ( E. y ph -> A. x ( A. y e. ( ( 1st ` x ) u. ( 2nd ` x ) ) ch -> ps ) )
15	9 14	exlimi	|- ( E. x E. y ph -> A. x ( A. y e. ( ( 1st ` x ) u. ( 2nd ` x ) ) ch -> ps ) )
16	6 8 1 2 15	pgindnf	|- ( E. x E. y ph -> ( A e. Pg -> th ) )
17	4 5 16	3syl	|- ( ph -> ( A e. Pg -> th ) )