Metamath Proof Explorer

Theorem dflim4

Description: An alternate definition of a limit ordinal. (Contributed by NM, 1-Feb-2005)

Ref Expression
Assertion dflim4 ⊢ Lim ⁡ A ↔ Ord ⁡ A ∧ ∅ ∈ A ∧ ∀ x ∈ A suc ⁡ x ∈ A

Proof

Step Hyp Ref Expression
1 dflim2 ⊢ Lim ⁡ A ↔ Ord ⁡ A ∧ ∅ ∈ A ∧ A = ⋃ A
2 ordunisuc2 ⊢ Ord ⁡ A → A = ⋃ A ↔ ∀ x ∈ A suc ⁡ x ∈ A
3 2 anbi2d ⊢ Ord ⁡ A → ∅ ∈ A ∧ A = ⋃ A ↔ ∅ ∈ A ∧ ∀ x ∈ A suc ⁡ x ∈ A
4 3 pm5.32i ⊢ Ord ⁡ A ∧ ∅ ∈ A ∧ A = ⋃ A ↔ Ord ⁡ A ∧ ∅ ∈ A ∧ ∀ x ∈ A suc ⁡ x ∈ A
5 3anass ⊢ Ord ⁡ A ∧ ∅ ∈ A ∧ A = ⋃ A ↔ Ord ⁡ A ∧ ∅ ∈ A ∧ A = ⋃ A
6 3anass ⊢ Ord ⁡ A ∧ ∅ ∈ A ∧ ∀ x ∈ A suc ⁡ x ∈ A ↔ Ord ⁡ A ∧ ∅ ∈ A ∧ ∀ x ∈ A suc ⁡ x ∈ A
7 4 5 6 3bitr4i ⊢ Ord ⁡ A ∧ ∅ ∈ A ∧ A = ⋃ A ↔ Ord ⁡ A ∧ ∅ ∈ A ∧ ∀ x ∈ A suc ⁡ x ∈ A
8 1 7 bitri ⊢ Lim ⁡ A ↔ Ord ⁡ A ∧ ∅ ∈ A ∧ ∀ x ∈ A suc ⁡ x ∈ A