Metamath Proof Explorer

Theorem enp1iOLD

Description: Obsolete version of enp1i as of 6-Jan-2025. (Contributed by Mario Carneiro, 5-Jan-2016) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 enp1iOLD.1 
 |-  M e. _om
2 enp1iOLD.2 
 |-  N = suc M
3 enp1iOLD.3 
 |-  ( ( A \ { x } ) ~~ M -> ph )
4 enp1iOLD.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 biimtrdi 
 |-  ( 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 dif1ennn 
 |-  ( ( 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 )