Theorem pgind

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

	Ref	Expression
Hypotheses	pgind.1	$$⊢x=y\to \left(\psi \leftrightarrow \chi \right)$$
	pgind.2	$$⊢y=A\to \left(\chi \leftrightarrow \theta \right)$$
	pgind.3	$$⊢\phi \to \forall x\left(\forall y\in \left(1^{st}\left(x\right)\cup 2^{nd}\left(x\right)\right)\chi \to \psi \right)$$
Assertion	pgind	$$⊢\phi \to \left(A\in \mathrm{Pg}\to \theta \right)$$

Proof

Step	Hyp	Ref	Expression
1		pgind.1	$$⊢x=y\to \left(\psi \leftrightarrow \chi \right)$$
2		pgind.2	$$⊢y=A\to \left(\chi \leftrightarrow \theta \right)$$
3		pgind.3	$$⊢\phi \to \forall x\left(\forall y\in \left(1^{st}\left(x\right)\cup 2^{nd}\left(x\right)\right)\chi \to \psi \right)$$
4		19.8a	$$⊢\phi \to \exists y\phi$$
5		19.8a	$$⊢\exists y\phi \to \exists x\exists y\phi$$
6		nfe1	$$⊢Ⅎx\exists x\exists y\phi$$
7		nfe1	$$⊢Ⅎy\exists y\phi$$
8	7	nfex	$$⊢Ⅎy\exists x\exists y\phi$$
9		nfa1	$$⊢Ⅎx\forall x\left(\forall y\in \left(1^{st}\left(x\right)\cup 2^{nd}\left(x\right)\right)\chi \to \psi \right)$$
10		nfra1	$$⊢Ⅎy\forall y\in \left(1^{st}\left(x\right)\cup 2^{nd}\left(x\right)\right)\chi$$
11		nfv	$$⊢Ⅎy\psi$$
12	10 11	nfim	$$⊢Ⅎy\left(\forall y\in \left(1^{st}\left(x\right)\cup 2^{nd}\left(x\right)\right)\chi \to \psi \right)$$
13	12	nfal	$$⊢Ⅎy\forall x\left(\forall y\in \left(1^{st}\left(x\right)\cup 2^{nd}\left(x\right)\right)\chi \to \psi \right)$$
14	13 3	exlimi	$$⊢\exists y\phi \to \forall x\left(\forall y\in \left(1^{st}\left(x\right)\cup 2^{nd}\left(x\right)\right)\chi \to \psi \right)$$
15	9 14	exlimi	$$⊢\exists x\exists y\phi \to \forall x\left(\forall y\in \left(1^{st}\left(x\right)\cup 2^{nd}\left(x\right)\right)\chi \to \psi \right)$$
16	6 8 1 2 15	pgindnf	$$⊢\exists x\exists y\phi \to \left(A\in \mathrm{Pg}\to \theta \right)$$
17	4 5 16	3syl	$$⊢\phi \to \left(A\in \mathrm{Pg}\to \theta \right)$$