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	syl6bbr	⊢ ( Ord 𝐴 → ( ( 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴 ) ↔ ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )
9	8	pm5.32i	⊢ ( ( Ord 𝐴 ∧ ( 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴 ) ) ↔ ( Ord 𝐴 ∧ ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )
10	1 2 9	3bitri	⊢ ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )