Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Ordinals
onun2
Next ⟩
onordi
Metamath Proof Explorer
Ascii
Unicode
Theorem
onun2
Description:
The union of two ordinals is an ordinal.
(Contributed by
Scott Fenton
, 9-Aug-2024)
Ref
Expression
Assertion
onun2
⊢
A
∈
On
∧
B
∈
On
→
A
∪
B
∈
On
Proof
Step
Hyp
Ref
Expression
1
ssequn1
⊢
A
⊆
B
↔
A
∪
B
=
B
2
eleq1a
⊢
B
∈
On
→
A
∪
B
=
B
→
A
∪
B
∈
On
3
2
adantl
⊢
A
∈
On
∧
B
∈
On
→
A
∪
B
=
B
→
A
∪
B
∈
On
4
1
3
syl5bi
⊢
A
∈
On
∧
B
∈
On
→
A
⊆
B
→
A
∪
B
∈
On
5
ssequn2
⊢
B
⊆
A
↔
A
∪
B
=
A
6
eleq1a
⊢
A
∈
On
→
A
∪
B
=
A
→
A
∪
B
∈
On
7
6
adantr
⊢
A
∈
On
∧
B
∈
On
→
A
∪
B
=
A
→
A
∪
B
∈
On
8
5
7
syl5bi
⊢
A
∈
On
∧
B
∈
On
→
B
⊆
A
→
A
∪
B
∈
On
9
eloni
⊢
A
∈
On
→
Ord
⁡
A
10
eloni
⊢
B
∈
On
→
Ord
⁡
B
11
ordtri2or2
⊢
Ord
⁡
A
∧
Ord
⁡
B
→
A
⊆
B
∨
B
⊆
A
12
9
10
11
syl2an
⊢
A
∈
On
∧
B
∈
On
→
A
⊆
B
∨
B
⊆
A
13
4
8
12
mpjaod
⊢
A
∈
On
∧
B
∈
On
→
A
∪
B
∈
On