Theorem bnj529

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

	Ref	Expression
Hypothesis	bnj529.1	⊢ 𝐷 = ( ω ∖ { ∅ } )
Assertion	bnj529	⊢ ( 𝑀 ∈ 𝐷 → ∅ ∈ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		bnj529.1	⊢ 𝐷 = ( ω ∖ { ∅ } )
2		eldifsn	⊢ ( 𝑀 ∈ ( ω ∖ { ∅ } ) ↔ ( 𝑀 ∈ ω ∧ 𝑀 ≠ ∅ ) )
3	2	biimpi	⊢ ( 𝑀 ∈ ( ω ∖ { ∅ } ) → ( 𝑀 ∈ ω ∧ 𝑀 ≠ ∅ ) )
4	3 1	eleq2s	⊢ ( 𝑀 ∈ 𝐷 → ( 𝑀 ∈ ω ∧ 𝑀 ≠ ∅ ) )
5		nnord	⊢ ( 𝑀 ∈ ω → Ord 𝑀 )
6	5	anim1i	⊢ ( ( 𝑀 ∈ ω ∧ 𝑀 ≠ ∅ ) → ( Ord 𝑀 ∧ 𝑀 ≠ ∅ ) )
7		ord0eln0	⊢ ( Ord 𝑀 → ( ∅ ∈ 𝑀 ↔ 𝑀 ≠ ∅ ) )
8	7	biimpar	⊢ ( ( Ord 𝑀 ∧ 𝑀 ≠ ∅ ) → ∅ ∈ 𝑀 )
9	4 6 8	3syl	⊢ ( 𝑀 ∈ 𝐷 → ∅ ∈ 𝑀 )