Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Ordinal arithmetic
nlim1
Next ⟩
nlim2
Metamath Proof Explorer
Ascii
Unicode
Theorem
nlim1
Description:
1 is not a limit ordinal.
(Contributed by
BTernaryTau
, 1-Dec-2024)
Ref
Expression
Assertion
nlim1
⊢
¬
Lim
⁡
1
𝑜
Proof
Step
Hyp
Ref
Expression
1
1n0
⊢
1
𝑜
≠
∅
2
0ex
⊢
∅
∈
V
3
2
unisn
⊢
⋃
∅
=
∅
4
1
3
neeqtrri
⊢
1
𝑜
≠
⋃
∅
5
df1o2
⊢
1
𝑜
=
∅
6
5
unieqi
⊢
⋃
1
𝑜
=
⋃
∅
7
4
6
neeqtrri
⊢
1
𝑜
≠
⋃
1
𝑜
8
7
neii
⊢
¬
1
𝑜
=
⋃
1
𝑜
9
simp3
⊢
Ord
⁡
1
𝑜
∧
1
𝑜
≠
∅
∧
1
𝑜
=
⋃
1
𝑜
→
1
𝑜
=
⋃
1
𝑜
10
8
9
mto
⊢
¬
Ord
⁡
1
𝑜
∧
1
𝑜
≠
∅
∧
1
𝑜
=
⋃
1
𝑜
11
df-lim
⊢
Lim
⁡
1
𝑜
↔
Ord
⁡
1
𝑜
∧
1
𝑜
≠
∅
∧
1
𝑜
=
⋃
1
𝑜
12
10
11
mtbir
⊢
¬
Lim
⁡
1
𝑜