Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Ordinal arithmetic
0lt1o
Next ⟩
dif20el
Metamath Proof Explorer
Ascii
Structured
Theorem
0lt1o
Description:
Ordinal zero is less than ordinal one.
(Contributed by
NM
, 5-Jan-2005)
Ref
Expression
Assertion
0lt1o
⊢
∅ ∈ 1
_{o}
Proof
Step
Hyp
Ref
Expression
1
eqid
⊢
∅ = ∅
2
el1o
⊢
( ∅ ∈ 1
_{o}
↔ ∅ = ∅ )
3
1
2
mpbir
⊢
∅ ∈ 1
_{o}