# Metamath Proof Explorer

## Theorem dflim4

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

Ref Expression
Assertion dflim4 ${⊢}\mathrm{Lim}{A}↔\left(\mathrm{Ord}{A}\wedge \varnothing \in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{x}\in {A}\right)$

### Proof

Step Hyp Ref Expression
1 dflim2 ${⊢}\mathrm{Lim}{A}↔\left(\mathrm{Ord}{A}\wedge \varnothing \in {A}\wedge {A}=\bigcup {A}\right)$
2 ordunisuc2 ${⊢}\mathrm{Ord}{A}\to \left({A}=\bigcup {A}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{x}\in {A}\right)$
3 2 anbi2d ${⊢}\mathrm{Ord}{A}\to \left(\left(\varnothing \in {A}\wedge {A}=\bigcup {A}\right)↔\left(\varnothing \in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{x}\in {A}\right)\right)$
4 3 pm5.32i ${⊢}\left(\mathrm{Ord}{A}\wedge \left(\varnothing \in {A}\wedge {A}=\bigcup {A}\right)\right)↔\left(\mathrm{Ord}{A}\wedge \left(\varnothing \in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{x}\in {A}\right)\right)$
5 3anass ${⊢}\left(\mathrm{Ord}{A}\wedge \varnothing \in {A}\wedge {A}=\bigcup {A}\right)↔\left(\mathrm{Ord}{A}\wedge \left(\varnothing \in {A}\wedge {A}=\bigcup {A}\right)\right)$
6 3anass ${⊢}\left(\mathrm{Ord}{A}\wedge \varnothing \in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{x}\in {A}\right)↔\left(\mathrm{Ord}{A}\wedge \left(\varnothing \in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{x}\in {A}\right)\right)$
7 4 5 6 3bitr4i ${⊢}\left(\mathrm{Ord}{A}\wedge \varnothing \in {A}\wedge {A}=\bigcup {A}\right)↔\left(\mathrm{Ord}{A}\wedge \varnothing \in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{x}\in {A}\right)$
8 1 7 bitri ${⊢}\mathrm{Lim}{A}↔\left(\mathrm{Ord}{A}\wedge \varnothing \in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{x}\in {A}\right)$