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∈Asuc⁡b∈A∧A≠∅

Proof

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