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

Metamath Proof Explorer

Theorem dflim4

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

Ref Expression
Assertion dflim4 ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 dflim2 ⊢ ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴 ) )
2 ordunisuc2 ⊢ ( Ord 𝐴 → ( 𝐴 = ∪ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) )
3 2 anbi2d ⊢ ( Ord 𝐴 → ( ( ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴 ) ↔ ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) ) )
4 3 pm5.32i ⊢ ( ( Ord 𝐴 ∧ ( ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴 ) ) ↔ ( Ord 𝐴 ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) ) )
5 3anass ⊢ ( ( Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴 ) ↔ ( Ord 𝐴 ∧ ( ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴 ) ) )
6 3anass ⊢ ( ( Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) ↔ ( Ord 𝐴 ∧ ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) ) )
7 4 5 6 3bitr4i ⊢ ( ( Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴 ) ↔ ( Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) )
8 1 7 bitri ⊢ ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) )