This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem enp1i

Description: Proof induction for en2 and related theorems. (Contributed by Mario Carneiro, 5-Jan-2016) Generalize to all ordinals and avoid ax-pow , ax-un . (Revised by BTernaryTau, 6-Jan-2025)

Ref Expression
Hypotheses enp1i.1 
|- Ord M
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 
 |-  Ord M
2 enp1i.2 
 |-  N = suc M
3 enp1i.3 
 |-  ( ( A \ { x } ) ~~ M -> ph )
4 enp1i.4 
 |-  ( x e. A -> ( ph -> ps ) )
5 2 breq2i 
 |-  ( A ~~ N <-> A ~~ suc M )
6 encv 
 |-  ( A ~~ suc M -> ( A e. _V /\ suc M e. _V ) )
7 6 simprd 
 |-  ( A ~~ suc M -> suc M e. _V )
8 sssucid 
 |-  M C_ suc M
9 ssexg 
 |-  ( ( M C_ suc M /\ suc M e. _V ) -> M e. _V )
10 8 9 mpan 
 |-  ( suc M e. _V -> M e. _V )
11 elong 
 |-  ( M e. _V -> ( M e. On <-> Ord M ) )
12 7 10 11 3syl 
 |-  ( A ~~ suc M -> ( M e. On <-> Ord M ) )
13 1 12 mpbiri 
 |-  ( A ~~ suc M -> M e. On )
14 rexdif1en 
 |-  ( ( M e. On /\ A ~~ suc M ) -> E. x e. A ( A \ { x } ) ~~ M )
15 13 14 mpancom 
 |-  ( A ~~ suc M -> E. x e. A ( A \ { x } ) ~~ M )
16 3 reximi 
 |-  ( E. x e. A ( A \ { x } ) ~~ M -> E. x e. A ph )
17 df-rex 
 |-  ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
18 4 imp 
 |-  ( ( x e. A /\ ph ) -> ps )
19 18 eximi 
 |-  ( E. x ( x e. A /\ ph ) -> E. x ps )
20 17 19 sylbi 
 |-  ( E. x e. A ph -> E. x ps )
21 15 16 20 3syl 
 |-  ( A ~~ suc M -> E. x ps )
22 5 21 sylbi 
 |-  ( A ~~ N -> E. x ps )