Theorem enp1i 7815

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

Hypotheses

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

Assertion

Ref	Expression
enp1i	|- ( A ~~ N -> E. x ps )

Distinct variable groups:   x, A   x, N

Allowed substitution hints:   ph( x)   ps( x)   M( x)

Proof of Theorem enp1i

Step	Hyp	Ref	Expression
1		nsuceq0 5522	. . . . 5 |- suc M =/= (/)
2		breq1 4426	. . . . . . 7 |- ( A = (/) -> ( A ~~ N <-> (/) ~~ N ) )
3		enp1i.2	. . . . . . . 8 |- N = suc M
4		ensym 7628	. . . . . . . . 9 |- ( (/) ~~ N -> N ~~ (/) )
5		en0 7642	. . . . . . . . 9 |- ( N ~~ (/) <-> N = (/) )
6	4, 5	sylib 199	. . . . . . . 8 |- ( (/) ~~ N -> N = (/) )
7	3, 6	syl5eqr 2477	. . . . . . 7 |- ( (/) ~~ N -> suc M = (/) )
8	2, 7	syl6bi 231	. . . . . 6 |- ( A = (/) -> ( A ~~ N -> suc M = (/) ) )
9	8	necon3ad 2630	. . . . 5 |- ( A = (/) -> ( suc M =/= (/) -> -. A ~~ N ) )
10	1, 9	mpi 20	. . . 4 |- ( A = (/) -> -. A ~~ N )
11	10	con2i 123	. . 3 |- ( A ~~ N -> -. A = (/) )
12		neq0 3772	. . 3 |- ( -. A = (/) <-> E. x x e. A )
13	11, 12	sylib 199	. 2 |- ( A ~~ N -> E. x x e. A )
14	3	breq2i 4431	. . . . 5 |- ( A ~~ N <-> A ~~ suc M )
15		enp1i.1	. . . . . . . 8 |- M e. om
16		dif1en 7813	. . . . . . . 8 |- ( ( M e. om /\ A ~~ suc M /\ x e. A ) -> ( A \ { x } ) ~~ M )
17	15, 16	mp3an1 1347	. . . . . . 7 |- ( ( A ~~ suc M /\ x e. A ) -> ( A \ { x } ) ~~ M )
18		enp1i.3	. . . . . . 7 |- ( ( A \ { x } ) ~~ M -> ph )
19	17, 18	syl 17	. . . . . 6 |- ( ( A ~~ suc M /\ x e. A ) -> ph )
20	19	ex 435	. . . . 5 |- ( A ~~ suc M -> ( x e. A -> ph ) )
21	14, 20	sylbi 198	. . . 4 |- ( A ~~ N -> ( x e. A -> ph ) )
22		enp1i.4	. . . 4 |- ( x e. A -> ( ph -> ps ) )
23	21, 22	sylcom 30	. . 3 |- ( A ~~ N -> ( x e. A -> ps ) )
24	23	eximdv 1758	. 2 |- ( A ~~ N -> ( E. x x e. A -> E. x ps ) )
25	13, 24	mpd 15	1 |- ( A ~~ N -> E. x ps )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 370   = wceq 1437   E.wex 1657   e. wcel 1872   =/= wne 2614   \ cdif 3433   (/)c0 3761   {csn 3998   class class class wbr 4423   suc csuc 5444   omcom 6706   ~~ cen 7577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-om 6707  df-1o 7193  df-er 7374  df-en 7581  df-fin 7584

This theorem is referenced by:  en2  7816  en3  7817  en4  7818