Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Ordinal arithmetic
oawordexr
Next ⟩
oawordex
Metamath Proof Explorer
Ascii
Unicode
Theorem
oawordexr
Description:
Existence theorem for weak ordering of ordinal sum.
(Contributed by
NM
, 12-Dec-2004)
Ref
Expression
Assertion
oawordexr
⊢
A
∈
On
∧
∃
x
∈
On
A
+
𝑜
x
=
B
→
A
⊆
B
Proof
Step
Hyp
Ref
Expression
1
oaword1
⊢
A
∈
On
∧
x
∈
On
→
A
⊆
A
+
𝑜
x
2
sseq2
⊢
A
+
𝑜
x
=
B
→
A
⊆
A
+
𝑜
x
↔
A
⊆
B
3
1
2
syl5ibcom
⊢
A
∈
On
∧
x
∈
On
→
A
+
𝑜
x
=
B
→
A
⊆
B
4
3
rexlimdva
⊢
A
∈
On
→
∃
x
∈
On
A
+
𝑜
x
=
B
→
A
⊆
B
5
4
imp
⊢
A
∈
On
∧
∃
x
∈
On
A
+
𝑜
x
=
B
→
A
⊆
B