Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Ordinals (continued)
orduni
Next ⟩
onint
Metamath Proof Explorer
Ascii
Unicode
Theorem
orduni
Description:
The union of an ordinal class is ordinal.
(Contributed by
NM
, 12-Sep-2003)
Ref
Expression
Assertion
orduni
⊢
Ord
⁡
A
→
Ord
⁡
⋃
A
Proof
Step
Hyp
Ref
Expression
1
ordsson
⊢
Ord
⁡
A
→
A
⊆
On
2
ssorduni
⊢
A
⊆
On
→
Ord
⁡
⋃
A
3
1
2
syl
⊢
Ord
⁡
A
→
Ord
⁡
⋃
A