This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑥 ) ) )