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

Metamath Proof Explorer

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 𝐴 )