Metamath Proof Explorer

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 ⊢ D = ω ∖ ∅
Assertion bnj529 ⊢ M ∈ D → ∅ ∈ M

Proof

Step Hyp Ref Expression
1 bnj529.1 ⊢ D = ω ∖ ∅
2 eldifsn ⊢ M ∈ ω ∖ ∅ ↔ M ∈ ω ∧ M ≠ ∅
3 2 biimpi ⊢ M ∈ ω ∖ ∅ → M ∈ ω ∧ M ≠ ∅
4 3 1 eleq2s ⊢ M ∈ D → M ∈ ω ∧ M ≠ ∅
5 nnord ⊢ M ∈ ω → Ord ⁡ M
6 5 anim1i ⊢ M ∈ ω ∧ M ≠ ∅ → Ord ⁡ M ∧ M ≠ ∅
7 ord0eln0 ⊢ Ord ⁡ M → ∅ ∈ M ↔ M ≠ ∅
8 7 biimpar ⊢ Ord ⁡ M ∧ M ≠ ∅ → ∅ ∈ M
9 4 6 8 3syl ⊢ M ∈ D → ∅ ∈ M