Metamath Proof Explorer

Theorem dflim6

Description: A limit ordinal is a non-zero ordinal which is not a successor ordinal. Definition 1.11 of Schloeder p. 2. (Contributed by RP, 16-Jan-2025)

Ref Expression
Assertion dflim6 ⊢ Lim ⁡ A ↔ Ord ⁡ A ∧ A ≠ ∅ ∧ ¬ ∃ b ∈ On A = suc ⁡ b

Proof

Step Hyp Ref Expression
1 ioran ⊢ ¬ A = ∅ ∨ ∃ b ∈ On A = suc ⁡ b ↔ ¬ A = ∅ ∧ ¬ ∃ b ∈ On A = suc ⁡ b
2 df-ne ⊢ A ≠ ∅ ↔ ¬ A = ∅
3 2 anbi1i ⊢ A ≠ ∅ ∧ ¬ ∃ b ∈ On A = suc ⁡ b ↔ ¬ A = ∅ ∧ ¬ ∃ b ∈ On A = suc ⁡ b
4 1 3 bitr4i ⊢ ¬ A = ∅ ∨ ∃ b ∈ On A = suc ⁡ b ↔ A ≠ ∅ ∧ ¬ ∃ b ∈ On A = suc ⁡ b
5 4 anbi2i ⊢ Ord ⁡ A ∧ ¬ A = ∅ ∨ ∃ b ∈ On A = suc ⁡ b ↔ Ord ⁡ A ∧ A ≠ ∅ ∧ ¬ ∃ b ∈ On A = suc ⁡ b
6 dflim3 ⊢ Lim ⁡ A ↔ Ord ⁡ A ∧ ¬ A = ∅ ∨ ∃ b ∈ On A = suc ⁡ b
7 3anass ⊢ Ord ⁡ A ∧ A ≠ ∅ ∧ ¬ ∃ b ∈ On A = suc ⁡ b ↔ Ord ⁡ A ∧ A ≠ ∅ ∧ ¬ ∃ b ∈ On A = suc ⁡ b
8 5 6 7 3bitr4i ⊢ Lim ⁡ A ↔ Ord ⁡ A ∧ A ≠ ∅ ∧ ¬ ∃ b ∈ On A = suc ⁡ b