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 𝐴 ↔ ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ ∃ 𝑏 ∈ On 𝐴 = suc 𝑏 ) )

Proof

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