Metamath Proof Explorer

Theorem dflim7

Description: A limit ordinal is a non-zero ordinal that contains all the successors of its elements. Lemma 1.18 of Schloeder p. 2. Closely related to dflim4 . (Contributed by RP, 17-Jan-2025)

Ref Expression
Assertion dflim7 ⊢ Lim ⁡ A ↔ Ord ⁡ A ∧ ∀ b ∈ A suc ⁡ b ∈ A ∧ A ≠ ∅

Proof

Step Hyp Ref Expression
1 dflim4 ⊢ Lim ⁡ A ↔ Ord ⁡ A ∧ ∅ ∈ A ∧ ∀ b ∈ A suc ⁡ b ∈ A
2 ord0eln0 ⊢ Ord ⁡ A → ∅ ∈ A ↔ A ≠ ∅
3 2 anbi1d ⊢ Ord ⁡ A → ∅ ∈ A ∧ ∀ b ∈ A suc ⁡ b ∈ A ↔ A ≠ ∅ ∧ ∀ b ∈ A suc ⁡ b ∈ A
4 3 biancomd ⊢ Ord ⁡ A → ∅ ∈ A ∧ ∀ b ∈ A suc ⁡ b ∈ A ↔ ∀ b ∈ A suc ⁡ b ∈ A ∧ A ≠ ∅
5 4 pm5.32i ⊢ Ord ⁡ A ∧ ∅ ∈ A ∧ ∀ b ∈ A suc ⁡ b ∈ A ↔ Ord ⁡ A ∧ ∀ b ∈ A suc ⁡ b ∈ A ∧ A ≠ ∅
6 3anass ⊢ Ord ⁡ A ∧ ∅ ∈ A ∧ ∀ b ∈ A suc ⁡ b ∈ A ↔ Ord ⁡ A ∧ ∅ ∈ A ∧ ∀ b ∈ A suc ⁡ b ∈ A
7 3anass ⊢ Ord ⁡ A ∧ ∀ b ∈ A suc ⁡ b ∈ A ∧ A ≠ ∅ ↔ Ord ⁡ A ∧ ∀ b ∈ A suc ⁡ b ∈ A ∧ A ≠ ∅
8 5 6 7 3bitr4i ⊢ Ord ⁡ A ∧ ∅ ∈ A ∧ ∀ b ∈ A suc ⁡ b ∈ A ↔ Ord ⁡ A ∧ ∀ b ∈ A suc ⁡ b ∈ A ∧ A ≠ ∅
9 1 8 bitri ⊢ Lim ⁡ A ↔ Ord ⁡ A ∧ ∀ b ∈ A suc ⁡ b ∈ A ∧ A ≠ ∅