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

Metamath Proof Explorer

Theorem dflim2

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

Ref Expression
Assertion dflim2 ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴 ) )

Proof

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