Theorem ellimits

Description: Membership in the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012)

	Ref	Expression
Hypothesis	ellimits.1	|- A e. _V
Assertion	ellimits	|- ( A e. Limits <-> Lim A )

Proof

Step	Hyp	Ref	Expression
1		ellimits.1	|- A e. _V
2		df-limits	|- Limits = ( ( On i^i Fix Bigcup ) \ { (/) } )
3	2	eleq2i	|- ( A e. Limits <-> A e. ( ( On i^i Fix Bigcup ) \ { (/) } ) )
4		eldif	|- ( A e. ( ( On i^i Fix Bigcup ) \ { (/) } ) <-> ( A e. ( On i^i Fix Bigcup ) /\ -. A e. { (/) } ) )
5		3anan32	|- ( ( Ord A /\ A =/= (/) /\ A = U. A ) <-> ( ( Ord A /\ A = U. A ) /\ A =/= (/) ) )
6		df-lim	|- ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )
7		elin	|- ( A e. ( On i^i Fix Bigcup ) <-> ( A e. On /\ A e. Fix Bigcup ) )
8	1	elon	|- ( A e. On <-> Ord A )
9	1	elfix	|- ( A e. Fix Bigcup <-> A Bigcup A )
10	1	brbigcup	|- ( A Bigcup A <-> U. A = A )
11		eqcom	|- ( U. A = A <-> A = U. A )
12	9 10 11	3bitri	|- ( A e. Fix Bigcup <-> A = U. A )
13	8 12	anbi12i	|- ( ( A e. On /\ A e. Fix Bigcup ) <-> ( Ord A /\ A = U. A ) )
14	7 13	bitri	|- ( A e. ( On i^i Fix Bigcup ) <-> ( Ord A /\ A = U. A ) )
15	1	elsn	|- ( A e. { (/) } <-> A = (/) )
16	15	necon3bbii	|- ( -. A e. { (/) } <-> A =/= (/) )
17	14 16	anbi12i	|- ( ( A e. ( On i^i Fix Bigcup ) /\ -. A e. { (/) } ) <-> ( ( Ord A /\ A = U. A ) /\ A =/= (/) ) )
18	5 6 17	3bitr4ri	|- ( ( A e. ( On i^i Fix Bigcup ) /\ -. A e. { (/) } ) <-> Lim A )
19	3 4 18	3bitri	|- ( A e. Limits <-> Lim A )