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 )