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	syl5eqr	⊢ ( ∅ ≈ 𝑁 → 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	⊢ ( 𝐴 ≈ 𝑁 → ∃ 𝑥 𝜓 )