Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Ordinal arithmetic
1oelpr
Next ⟩
2oex
Metamath Proof Explorer
Ascii
Unicode
Theorem
1oelpr
Description:
1o
is an element of
{ (/) , 1o }
.
(Contributed by
Umit Teoman Dogan
, 10-Jun-2026)
Ref
Expression
Assertion
1oelpr
⊢
1
𝑜
∈
∅
1
𝑜
Proof
Step
Hyp
Ref
Expression
1
1oex
⊢
1
𝑜
∈
V
2
1
prid2
⊢
1
𝑜
∈
∅
1
𝑜