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 𝑀 ∈ ω
enp1i.2 𝑁 = suc 𝑀
enp1i.3 ( ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀𝜑 )
enp1i.4 ( 𝑥𝐴 → ( 𝜑𝜓 ) )
Assertion enp1i ( 𝐴𝑁 → ∃ 𝑥 𝜓 )

Proof

Step Hyp Ref Expression
1 enp1i.1 𝑀 ∈ ω
2 enp1i.2 𝑁 = suc 𝑀
3 enp1i.3 ( ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀𝜑 )
4 enp1i.4 ( 𝑥𝐴 → ( 𝜑𝜓 ) )
5 nsuceq0 suc 𝑀 ≠ ∅
6 breq1 ( 𝐴 = ∅ → ( 𝐴𝑁 ↔ ∅ ≈ 𝑁 ) )
7 ensym ( ∅ ≈ 𝑁𝑁 ≈ ∅ )
8 en0 ( 𝑁 ≈ ∅ ↔ 𝑁 = ∅ )
9 7 8 sylib ( ∅ ≈ 𝑁𝑁 = ∅ )
10 2 9 eqtr3id ( ∅ ≈ 𝑁 → suc 𝑀 = ∅ )
11 6 10 syl6bi ( 𝐴 = ∅ → ( 𝐴𝑁 → suc 𝑀 = ∅ ) )
12 11 necon3ad ( 𝐴 = ∅ → ( suc 𝑀 ≠ ∅ → ¬ 𝐴𝑁 ) )
13 5 12 mpi ( 𝐴 = ∅ → ¬ 𝐴𝑁 )
14 13 con2i ( 𝐴𝑁 → ¬ 𝐴 = ∅ )
15 neq0 ( ¬ 𝐴 = ∅ ↔ ∃ 𝑥 𝑥𝐴 )
16 14 15 sylib ( 𝐴𝑁 → ∃ 𝑥 𝑥𝐴 )
17 2 breq2i ( 𝐴𝑁𝐴 ≈ suc 𝑀 )
18 dif1en ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑥𝐴 ) → ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 )
19 1 18 mp3an1 ( ( 𝐴 ≈ suc 𝑀𝑥𝐴 ) → ( 𝐴 ∖ { 𝑥 } ) ≈ 𝑀 )
20 19 3 syl ( ( 𝐴 ≈ suc 𝑀𝑥𝐴 ) → 𝜑 )
21 20 ex ( 𝐴 ≈ suc 𝑀 → ( 𝑥𝐴𝜑 ) )
22 17 21 sylbi ( 𝐴𝑁 → ( 𝑥𝐴𝜑 ) )
23 22 4 sylcom ( 𝐴𝑁 → ( 𝑥𝐴𝜓 ) )
24 23 eximdv ( 𝐴𝑁 → ( ∃ 𝑥 𝑥𝐴 → ∃ 𝑥 𝜓 ) )
25 16 24 mpd ( 𝐴𝑁 → ∃ 𝑥 𝜓 )