Theorem ellimits

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

	Ref	Expression
Hypothesis	ellimits.1	⊢ 𝐴 ∈ V
Assertion	ellimits	⊢ ( 𝐴 ∈ Limits ↔ Lim 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ellimits.1	⊢ 𝐴 ∈ V
2		df-limits	⊢ Limits = ( ( On ∩ Fix Bigcup ) ∖ { ∅ } )
3	2	eleq2i	⊢ ( 𝐴 ∈ Limits ↔ 𝐴 ∈ ( ( On ∩ Fix Bigcup ) ∖ { ∅ } ) )
4		eldif	⊢ ( 𝐴 ∈ ( ( On ∩ Fix Bigcup ) ∖ { ∅ } ) ↔ ( 𝐴 ∈ ( On ∩ Fix Bigcup ) ∧ ¬ 𝐴 ∈ { ∅ } ) )
5		3anan32	⊢ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴 ) ↔ ( ( Ord 𝐴 ∧ 𝐴 = ∪ 𝐴 ) ∧ 𝐴 ≠ ∅ ) )
6		df-lim	⊢ ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴 ) )
7		elin	⊢ ( 𝐴 ∈ ( On ∩ Fix Bigcup ) ↔ ( 𝐴 ∈ On ∧ 𝐴 ∈ Fix Bigcup ) )
8	1	elon	⊢ ( 𝐴 ∈ On ↔ Ord 𝐴 )
9	1	elfix	⊢ ( 𝐴 ∈ Fix Bigcup ↔ 𝐴 Bigcup 𝐴 )
10	1	brbigcup	⊢ ( 𝐴 Bigcup 𝐴 ↔ ∪ 𝐴 = 𝐴 )
11		eqcom	⊢ ( ∪ 𝐴 = 𝐴 ↔ 𝐴 = ∪ 𝐴 )
12	9 10 11	3bitri	⊢ ( 𝐴 ∈ Fix Bigcup ↔ 𝐴 = ∪ 𝐴 )
13	8 12	anbi12i	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ∈ Fix Bigcup ) ↔ ( Ord 𝐴 ∧ 𝐴 = ∪ 𝐴 ) )
14	7 13	bitri	⊢ ( 𝐴 ∈ ( On ∩ Fix Bigcup ) ↔ ( Ord 𝐴 ∧ 𝐴 = ∪ 𝐴 ) )
15	1	elsn	⊢ ( 𝐴 ∈ { ∅ } ↔ 𝐴 = ∅ )
16	15	necon3bbii	⊢ ( ¬ 𝐴 ∈ { ∅ } ↔ 𝐴 ≠ ∅ )
17	14 16	anbi12i	⊢ ( ( 𝐴 ∈ ( On ∩ Fix Bigcup ) ∧ ¬ 𝐴 ∈ { ∅ } ) ↔ ( ( Ord 𝐴 ∧ 𝐴 = ∪ 𝐴 ) ∧ 𝐴 ≠ ∅ ) )
18	5 6 17	3bitr4ri	⊢ ( ( 𝐴 ∈ ( On ∩ Fix Bigcup ) ∧ ¬ 𝐴 ∈ { ∅ } ) ↔ Lim 𝐴 )
19	3 4 18	3bitri	⊢ ( 𝐴 ∈ Limits ↔ Lim 𝐴 )