Metamath Proof Explorer


Theorem enp1i

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

Ref Expression
Hypotheses enp1i.1 M ω
enp1i.2 N = suc M
enp1i.3 A x M φ
enp1i.4 x A φ ψ
Assertion enp1i A N x ψ

Proof

Step Hyp Ref Expression
1 enp1i.1 M ω
2 enp1i.2 N = suc M
3 enp1i.3 A x M φ
4 enp1i.4 x A φ ψ
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 = x x A
16 14 15 sylib A N x x A
17 2 breq2i A N A suc M
18 dif1en M ω A suc M x A A x M
19 1 18 mp3an1 A suc M x A A x M
20 19 3 syl A suc M x A φ
21 20 ex A suc M x A φ
22 17 21 sylbi A N x A φ
23 22 4 sylcom A N x A ψ
24 23 eximdv A N x x A x ψ
25 16 24 mpd A N x ψ