Theorem enp1i

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

	Ref	Expression
Hypotheses	enp1i.1	|- M e. _om
	enp1i.2	|- N = suc M
	enp1i.3	|- ( ( A \ { x } ) ~~ M -> ph )
	enp1i.4	|- ( x e. A -> ( ph -> ps ) )
Assertion	enp1i	|- ( A ~~ N -> E. x ps )

Proof

Step	Hyp	Ref	Expression
1		enp1i.1	|- M e. _om
2		enp1i.2	|- N = suc M
3		enp1i.3	|- ( ( A \ { x } ) ~~ M -> ph )
4		enp1i.4	|- ( x e. A -> ( ph -> ps ) )
5		nsuceq0	|- suc M =/= (/)
6		breq1	|- ( A = (/) -> ( A ~~ N <-> (/) ~~ N ) )
7		ensym	|- ( (/) ~~ N -> N ~~ (/) )
8		en0	|- ( N ~~ (/) <-> N = (/) )
9	7 8	sylib	|- ( (/) ~~ N -> N = (/) )
10	2 9	eqtr3id	|- ( (/) ~~ N -> suc M = (/) )
11	6 10	syl6bi	|- ( A = (/) -> ( A ~~ N -> suc M = (/) ) )
12	11	necon3ad	|- ( A = (/) -> ( suc M =/= (/) -> -. A ~~ N ) )
13	5 12	mpi	|- ( A = (/) -> -. A ~~ N )
14	13	con2i	|- ( A ~~ N -> -. A = (/) )
15		neq0	|- ( -. A = (/) <-> E. x x e. A )
16	14 15	sylib	|- ( A ~~ N -> E. x x e. A )
17	2	breq2i	|- ( A ~~ N <-> A ~~ suc M )
18		dif1en	|- ( ( M e. _om /\ A ~~ suc M /\ x e. A ) -> ( A \ { x } ) ~~ M )
19	1 18	mp3an1	|- ( ( A ~~ suc M /\ x e. A ) -> ( A \ { x } ) ~~ M )
20	19 3	syl	|- ( ( A ~~ suc M /\ x e. A ) -> ph )
21	20	ex	|- ( A ~~ suc M -> ( x e. A -> ph ) )
22	17 21	sylbi	|- ( A ~~ N -> ( x e. A -> ph ) )
23	22 4	sylcom	|- ( A ~~ N -> ( x e. A -> ps ) )
24	23	eximdv	|- ( A ~~ N -> ( E. x x e. A -> E. x ps ) )
25	16 24	mpd	|- ( A ~~ N -> E. x ps )