This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 bitr2id ⊢ ( 𝑚 ∈ ω → ( 𝑚 = ∅ ↔ suc 𝑚 = 1o ) )
15 14 necon3bid ⊢ ( 𝑚 ∈ ω → ( 𝑚 ≠ ∅ ↔ suc 𝑚 ≠ 1o ) )
16 7 15 imbitrrid ⊢ ( 𝑚 ∈ ω → ( ( 𝑛 ≠ 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 𝑚 )