Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Ordinal arithmetic
2ellim
Next ⟩
dif1o
Metamath Proof Explorer
Ascii
Unicode
Theorem
2ellim
Description:
A limit ordinal contains 2.
(Contributed by
BTernaryTau
, 1-Dec-2024)
Ref
Expression
Assertion
2ellim
⊢
Lim
⁡
A
→
2
𝑜
∈
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
nlim2
⊢
¬
Lim
⁡
2
𝑜
10
limeq
⊢
A
=
2
𝑜
→
Lim
⁡
A
↔
Lim
⁡
2
𝑜
11
9
10
mtbiri
⊢
A
=
2
𝑜
→
¬
Lim
⁡
A
12
11
necon2ai
⊢
Lim
⁡
A
→
A
≠
2
𝑜
13
limord
⊢
Lim
⁡
A
→
Ord
⁡
A
14
ord2eln012
⊢
Ord
⁡
A
→
2
𝑜
∈
A
↔
A
≠
∅
∧
A
≠
1
𝑜
∧
A
≠
2
𝑜
15
13
14
syl
⊢
Lim
⁡
A
→
2
𝑜
∈
A
↔
A
≠
∅
∧
A
≠
1
𝑜
∧
A
≠
2
𝑜
16
4
8
12
15
mpbir3and
⊢
Lim
⁡
A
→
2
𝑜
∈
A