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 ⊢ A ∈ V
Assertion ellimits ⊢ A ∈ 𝖫𝗂𝗆𝗂𝗍𝗌 ↔ Lim ⁡ A

Proof

Step Hyp Ref Expression
1 ellimits.1 ⊢ A ∈ V
2 df-limits ⊢ 𝖫𝗂𝗆𝗂𝗍𝗌 = On ∩ 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉 ∖ ∅
3 2 eleq2i ⊢ A ∈ 𝖫𝗂𝗆𝗂𝗍𝗌 ↔ A ∈ On ∩ 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉 ∖ ∅
4 eldif ⊢ A ∈ On ∩ 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉 ∖ ∅ ↔ A ∈ On ∩ 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉 ∧ ¬ A ∈ ∅
5 3anan32 ⊢ Ord ⁡ A ∧ A ≠ ∅ ∧ A = ⋃ A ↔ Ord ⁡ A ∧ A = ⋃ A ∧ A ≠ ∅
6 df-lim ⊢ Lim ⁡ A ↔ Ord ⁡ A ∧ A ≠ ∅ ∧ A = ⋃ A
7 elin ⊢ A ∈ On ∩ 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉 ↔ A ∈ On ∧ A ∈ 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉
8 1 elon ⊢ A ∈ On ↔ Ord ⁡ A
9 1 elfix ⊢ A ∈ 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉 ↔ A 𝖡𝗂𝗀𝖼𝗎𝗉 A
10 1 brbigcup ⊢ A 𝖡𝗂𝗀𝖼𝗎𝗉 A ↔ ⋃ A = A
11 eqcom ⊢ ⋃ A = A ↔ A = ⋃ A
12 9 10 11 3bitri ⊢ A ∈ 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉 ↔ A = ⋃ A
13 8 12 anbi12i ⊢ A ∈ On ∧ A ∈ 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉 ↔ Ord ⁡ A ∧ A = ⋃ A
14 7 13 bitri ⊢ A ∈ On ∩ 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉 ↔ Ord ⁡ A ∧ A = ⋃ A
15 1 elsn ⊢ A ∈ ∅ ↔ A = ∅
16 15 necon3bbii ⊢ ¬ A ∈ ∅ ↔ A ≠ ∅
17 14 16 anbi12i ⊢ A ∈ On ∩ 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉 ∧ ¬ A ∈ ∅ ↔ Ord ⁡ A ∧ A = ⋃ A ∧ A ≠ ∅
18 5 6 17 3bitr4ri ⊢ A ∈ On ∩ 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉 ∧ ¬ A ∈ ∅ ↔ Lim ⁡ A
19 3 4 18 3bitri ⊢ A ∈ 𝖫𝗂𝗆𝗂𝗍𝗌 ↔ Lim ⁡ A