Theorem bnj168

Description: First-order logic and set theory. Revised to remove dependence on ax-reg . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Revised by NM, 21-Dec-2016) (New usage is discouraged.)

	Ref	Expression
Hypothesis	bnj168.1	⊢ 𝐷 = ( ω ∖ { ∅ } )
Assertion	bnj168	⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∈ 𝐷 𝑛 = suc 𝑚 )

Proof

Step	Hyp	Ref	Expression
1		bnj168.1	⊢ 𝐷 = ( ω ∖ { ∅ } )
2	1	bnj158	⊢ ( 𝑛 ∈ 𝐷 → ∃ 𝑚 ∈ ω 𝑛 = suc 𝑚 )
3	2	anim2i	⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ( 𝑛 ≠ 1o ∧ ∃ 𝑚 ∈ ω 𝑛 = suc 𝑚 ) )
4		r19.42v	⊢ ( ∃ 𝑚 ∈ ω ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) ↔ ( 𝑛 ≠ 1o ∧ ∃ 𝑚 ∈ ω 𝑛 = suc 𝑚 ) )
5	3 4	sylibr	⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∈ ω ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) )
6		neeq1	⊢ ( 𝑛 = suc 𝑚 → ( 𝑛 ≠ 1o ↔ suc 𝑚 ≠ 1o ) )
7	6	biimpac	⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) → suc 𝑚 ≠ 1o )
8		df-1o	⊢ 1o = suc ∅
9	8	eqeq2i	⊢ ( suc 𝑚 = 1o ↔ suc 𝑚 = suc ∅ )
10		nnon	⊢ ( 𝑚 ∈ ω → 𝑚 ∈ On )
11		0elon	⊢ ∅ ∈ On
12		suc11	⊢ ( ( 𝑚 ∈ On ∧ ∅ ∈ On ) → ( suc 𝑚 = suc ∅ ↔ 𝑚 = ∅ ) )
13	10 11 12	sylancl	⊢ ( 𝑚 ∈ ω → ( suc 𝑚 = suc ∅ ↔ 𝑚 = ∅ ) )
14	9 13	syl5rbb	⊢ ( 𝑚 ∈ ω → ( 𝑚 = ∅ ↔ suc 𝑚 = 1o ) )
15	14	necon3bid	⊢ ( 𝑚 ∈ ω → ( 𝑚 ≠ ∅ ↔ suc 𝑚 ≠ 1o ) )
16	7 15	syl5ibr	⊢ ( 𝑚 ∈ ω → ( ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) → 𝑚 ≠ ∅ ) )
17	16	ancld	⊢ ( 𝑚 ∈ ω → ( ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) → ( ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) ∧ 𝑚 ≠ ∅ ) ) )
18	17	reximia	⊢ ( ∃ 𝑚 ∈ ω ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) → ∃ 𝑚 ∈ ω ( ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) ∧ 𝑚 ≠ ∅ ) )
19	5 18	syl	⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∈ ω ( ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) ∧ 𝑚 ≠ ∅ ) )
20		anass	⊢ ( ( ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) ∧ 𝑚 ≠ ∅ ) ↔ ( 𝑛 ≠ 1o ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) )
21	20	rexbii	⊢ ( ∃ 𝑚 ∈ ω ( ( 𝑛 ≠ 1o ∧ 𝑛 = suc 𝑚 ) ∧ 𝑚 ≠ ∅ ) ↔ ∃ 𝑚 ∈ ω ( 𝑛 ≠ 1o ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) )
22	19 21	sylib	⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∈ ω ( 𝑛 ≠ 1o ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) )
23		simpr	⊢ ( ( 𝑛 ≠ 1o ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) → ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) )
24	22 23	bnj31	⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∈ ω ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) )
25		df-rex	⊢ ( ∃ 𝑚 ∈ ω ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ↔ ∃ 𝑚 ( 𝑚 ∈ ω ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) )
26	24 25	sylib	⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ( 𝑚 ∈ ω ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) )
27		simpr	⊢ ( ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) → 𝑚 ≠ ∅ )
28	27	anim2i	⊢ ( ( 𝑚 ∈ ω ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) → ( 𝑚 ∈ ω ∧ 𝑚 ≠ ∅ ) )
29	1	eleq2i	⊢ ( 𝑚 ∈ 𝐷 ↔ 𝑚 ∈ ( ω ∖ { ∅ } ) )
30		eldifsn	⊢ ( 𝑚 ∈ ( ω ∖ { ∅ } ) ↔ ( 𝑚 ∈ ω ∧ 𝑚 ≠ ∅ ) )
31	29 30	bitr2i	⊢ ( ( 𝑚 ∈ ω ∧ 𝑚 ≠ ∅ ) ↔ 𝑚 ∈ 𝐷 )
32	28 31	sylib	⊢ ( ( 𝑚 ∈ ω ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) → 𝑚 ∈ 𝐷 )
33		simprl	⊢ ( ( 𝑚 ∈ ω ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) → 𝑛 = suc 𝑚 )
34	32 33	jca	⊢ ( ( 𝑚 ∈ ω ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) → ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) )
35	34	eximi	⊢ ( ∃ 𝑚 ( 𝑚 ∈ ω ∧ ( 𝑛 = suc 𝑚 ∧ 𝑚 ≠ ∅ ) ) → ∃ 𝑚 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) )
36	26 35	syl	⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) )
37		df-rex	⊢ ( ∃ 𝑚 ∈ 𝐷 𝑛 = suc 𝑚 ↔ ∃ 𝑚 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ) )
38	36 37	sylibr	⊢ ( ( 𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑚 ∈ 𝐷 𝑛 = suc 𝑚 )