Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Ordinal arithmetic
1ellim
Next ⟩
2ellim
Metamath Proof Explorer
Ascii
Unicode
Theorem
1ellim
Description:
A limit ordinal contains 1.
(Contributed by
BTernaryTau
, 1-Dec-2024)
Ref
Expression
Assertion
1ellim
⊢
Lim
⁡
A
→
1
𝑜
∈
A
Proof
Step
Hyp
Ref
Expression
1
nlim0
⊢
¬
Lim
⁡
∅
2
limeq
⊢
A
=
∅
→
Lim
⁡
A
↔
Lim
⁡
∅
3
1
2
mtbiri
⊢
A
=
∅
→
¬
Lim
⁡
A
4
3
necon2ai
⊢
Lim
⁡
A
→
A
≠
∅
5
nlim1
⊢
¬
Lim
⁡
1
𝑜
6
limeq
⊢
A
=
1
𝑜
→
Lim
⁡
A
↔
Lim
⁡
1
𝑜
7
5
6
mtbiri
⊢
A
=
1
𝑜
→
¬
Lim
⁡
A
8
7
necon2ai
⊢
Lim
⁡
A
→
A
≠
1
𝑜
9
limord
⊢
Lim
⁡
A
→
Ord
⁡
A
10
ord1eln01
⊢
Ord
⁡
A
→
1
𝑜
∈
A
↔
A
≠
∅
∧
A
≠
1
𝑜
11
9
10
syl
⊢
Lim
⁡
A
→
1
𝑜
∈
A
↔
A
≠
∅
∧
A
≠
1
𝑜
12
4
8
11
mpbir2and
⊢
Lim
⁡
A
→
1
𝑜
∈
A