Theorem enp1i

Description: Proof induction for en2i and related theorems. (Contributed by Mario Carneiro, 5-Jan-2016)

	Ref	Expression
Hypotheses	enp1i.1	$$⊢M\in \mathrm{\omega }$$
	enp1i.2	$$⊢N=\mathrm{suc}M$$
	enp1i.3	$$⊢\left(A\setminus \left\{x\right\}\right)\approx M\to \phi$$
	enp1i.4	$$⊢x\in A\to \left(\phi \to \psi \right)$$
Assertion	enp1i	$$⊢A\approx N\to \exists x\psi$$

Proof

Step	Hyp	Ref	Expression
1		enp1i.1	$$⊢M\in \mathrm{\omega }$$
2		enp1i.2	$$⊢N=\mathrm{suc}M$$
3		enp1i.3	$$⊢\left(A\setminus \left\{x\right\}\right)\approx M\to \phi$$
4		enp1i.4	$$⊢x\in A\to \left(\phi \to \psi \right)$$
5		nsuceq0	$$⊢\mathrm{suc}M\ne \varnothing$$
6		breq1	$$⊢A=\varnothing \to \left(A\approx N\leftrightarrow \varnothing \approx N\right)$$
7		ensym	$$⊢\varnothing \approx N\to N\approx \varnothing$$
8		en0	$$⊢N\approx \varnothing \leftrightarrow N=\varnothing$$
9	7 8	sylib	$$⊢\varnothing \approx N\to N=\varnothing$$
10	2 9	syl5eqr	$$⊢\varnothing \approx N\to \mathrm{suc}M=\varnothing$$
11	6 10	syl6bi	$$⊢A=\varnothing \to \left(A\approx N\to \mathrm{suc}M=\varnothing \right)$$
12	11	necon3ad	$$⊢A=\varnothing \to \left(\mathrm{suc}M\ne \varnothing \to \neg A\approx N\right)$$
13	5 12	mpi	$$⊢A=\varnothing \to \neg A\approx N$$
14	13	con2i	$$⊢A\approx N\to \neg A=\varnothing$$
15		neq0	$$⊢\neg A=\varnothing \leftrightarrow \exists xx\in A$$
16	14 15	sylib	$$⊢A\approx N\to \exists xx\in A$$
17	2	breq2i	$$⊢A\approx N\leftrightarrow A\approx \mathrm{suc}M$$
18		dif1en	$$⊢\left(M\in \mathrm{\omega }\wedge A\approx \mathrm{suc}M\wedge x\in A\right)\to \left(A\setminus \left\{x\right\}\right)\approx M$$
19	1 18	mp3an1	$$⊢\left(A\approx \mathrm{suc}M\wedge x\in A\right)\to \left(A\setminus \left\{x\right\}\right)\approx M$$
20	19 3	syl	$$⊢\left(A\approx \mathrm{suc}M\wedge x\in A\right)\to \phi$$
21	20	ex	$$⊢A\approx \mathrm{suc}M\to \left(x\in A\to \phi \right)$$
22	17 21	sylbi	$$⊢A\approx N\to \left(x\in A\to \phi \right)$$
23	22 4	sylcom	$$⊢A\approx N\to \left(x\in A\to \psi \right)$$
24	23	eximdv	$$⊢A\approx N\to \left(\exists xx\in A\to \exists x\psi \right)$$
25	16 24	mpd	$$⊢A\approx N\to \exists x\psi$$