Metamath Proof Explorer

Theorem dflim2

Description: An alternate definition of a limit ordinal. (Contributed by NM, 4-Nov-2004)

Ref Expression
Assertion dflim2 ⊢ Lim ⁡ A ↔ Ord ⁡ A ∧ ∅ ∈ A ∧ A = ⋃ A

Proof

Step Hyp Ref Expression
1 df-lim ⊢ Lim ⁡ A ↔ Ord ⁡ A ∧ A ≠ ∅ ∧ A = ⋃ A
2 ord0eln0 ⊢ Ord ⁡ A → ∅ ∈ A ↔ A ≠ ∅
3 2 anbi1d ⊢ Ord ⁡ A → ∅ ∈ A ∧ A = ⋃ A ↔ A ≠ ∅ ∧ A = ⋃ A
4 3 pm5.32i ⊢ Ord ⁡ A ∧ ∅ ∈ A ∧ A = ⋃ A ↔ Ord ⁡ A ∧ A ≠ ∅ ∧ A = ⋃ A
5 3anass ⊢ Ord ⁡ A ∧ ∅ ∈ A ∧ A = ⋃ A ↔ Ord ⁡ A ∧ ∅ ∈ A ∧ A = ⋃ A
6 3anass ⊢ Ord ⁡ A ∧ A ≠ ∅ ∧ A = ⋃ A ↔ Ord ⁡ A ∧ A ≠ ∅ ∧ A = ⋃ A
7 4 5 6 3bitr4i ⊢ Ord ⁡ A ∧ ∅ ∈ A ∧ A = ⋃ A ↔ Ord ⁡ A ∧ A ≠ ∅ ∧ A = ⋃ A
8 1 7 bitr4i ⊢ Lim ⁡ A ↔ Ord ⁡ A ∧ ∅ ∈ A ∧ A = ⋃ A