Theorem bnj158

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypothesis	bnj158.1	⊢ 𝐷 = ( ω ∖ { ∅ } )
Assertion	bnj158	⊢ ( 𝑚 ∈ 𝐷 → ∃ 𝑝 ∈ ω 𝑚 = suc 𝑝 )

Proof

Step	Hyp	Ref	Expression
1		bnj158.1	⊢ 𝐷 = ( ω ∖ { ∅ } )
2	1	eleq2i	⊢ ( 𝑚 ∈ 𝐷 ↔ 𝑚 ∈ ( ω ∖ { ∅ } ) )
3		eldifsn	⊢ ( 𝑚 ∈ ( ω ∖ { ∅ } ) ↔ ( 𝑚 ∈ ω ∧ 𝑚 ≠ ∅ ) )
4	2 3	bitri	⊢ ( 𝑚 ∈ 𝐷 ↔ ( 𝑚 ∈ ω ∧ 𝑚 ≠ ∅ ) )
5		nnsuc	⊢ ( ( 𝑚 ∈ ω ∧ 𝑚 ≠ ∅ ) → ∃ 𝑝 ∈ ω 𝑚 = suc 𝑝 )
6	4 5	sylbi	⊢ ( 𝑚 ∈ 𝐷 → ∃ 𝑝 ∈ ω 𝑚 = suc 𝑝 )