Metamath Proof Explorer


Theorem dflim3

Description: An alternate definition of a limit ordinal, which is any ordinal that is neither zero nor a successor. (Contributed by NM, 1-Nov-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion dflim3 ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 df-lim ( Lim 𝐴 ↔ ( Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴 ) )
2 3anass ( ( Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴 ) ↔ ( Ord 𝐴 ∧ ( 𝐴 ≠ ∅ ∧ 𝐴 = 𝐴 ) ) )
3 df-ne ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
4 3 a1i ( Ord 𝐴 → ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ ) )
5 orduninsuc ( Ord 𝐴 → ( 𝐴 = 𝐴 ↔ ¬ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) )
6 4 5 anbi12d ( Ord 𝐴 → ( ( 𝐴 ≠ ∅ ∧ 𝐴 = 𝐴 ) ↔ ( ¬ 𝐴 = ∅ ∧ ¬ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )
7 ioran ( ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ↔ ( ¬ 𝐴 = ∅ ∧ ¬ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) )
8 6 7 bitr4di ( Ord 𝐴 → ( ( 𝐴 ≠ ∅ ∧ 𝐴 = 𝐴 ) ↔ ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )
9 8 pm5.32i ( ( Ord 𝐴 ∧ ( 𝐴 ≠ ∅ ∧ 𝐴 = 𝐴 ) ) ↔ ( Ord 𝐴 ∧ ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )
10 1 2 9 3bitri ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )