Theorem limom

Description: Omega is a limit ordinal. Theorem 2.8 of BellMachover p. 473. Our proof, however, does not require the Axiom of Infinity. (Contributed by NM, 26-Mar-1995) (Proof shortened by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Assertion	limom	|- Lim _om

Proof

Step	Hyp	Ref	Expression
1		ordom	|- Ord _om
2		ordeleqon	|- ( Ord _om <-> ( _om e. On \/ _om = On ) )
3		ordirr	|- ( Ord _om -> -. _om e. _om )
4	1 3	ax-mp	|- -. _om e. _om
5		elom	|- ( _om e. _om <-> ( _om e. On /\ A. x ( Lim x -> _om e. x ) ) )
6	5	baib	|- ( _om e. On -> ( _om e. _om <-> A. x ( Lim x -> _om e. x ) ) )
7	4 6	mtbii	|- ( _om e. On -> -. A. x ( Lim x -> _om e. x ) )
8		limomss	|- ( Lim x -> _om C_ x )
9		limord	|- ( Lim x -> Ord x )
10		ordsseleq	|- ( ( Ord _om /\ Ord x ) -> ( _om C_ x <-> ( _om e. x \/ _om = x ) ) )
11	1 9 10	sylancr	|- ( Lim x -> ( _om C_ x <-> ( _om e. x \/ _om = x ) ) )
12	8 11	mpbid	|- ( Lim x -> ( _om e. x \/ _om = x ) )
13	12	ord	|- ( Lim x -> ( -. _om e. x -> _om = x ) )
14		limeq	|- ( _om = x -> ( Lim _om <-> Lim x ) )
15	14	biimprcd	|- ( Lim x -> ( _om = x -> Lim _om ) )
16	13 15	syld	|- ( Lim x -> ( -. _om e. x -> Lim _om ) )
17	16	con1d	|- ( Lim x -> ( -. Lim _om -> _om e. x ) )
18	17	com12	|- ( -. Lim _om -> ( Lim x -> _om e. x ) )
19	18	alrimiv	|- ( -. Lim _om -> A. x ( Lim x -> _om e. x ) )
20	7 19	nsyl2	|- ( _om e. On -> Lim _om )
21		limon	|- Lim On
22		limeq	|- ( _om = On -> ( Lim _om <-> Lim On ) )
23	21 22	mpbiri	|- ( _om = On -> Lim _om )
24	20 23	jaoi	|- ( ( _om e. On \/ _om = On ) -> Lim _om )
25	2 24	sylbi	|- ( Ord _om -> Lim _om )
26	1 25	ax-mp	|- Lim _om