Metamath Proof Explorer

Theorem oaun3lem3

Description: The class of all ordinal sums of elements from two ordinals is an ordinal. Lemma for oaun3 . (Contributed by RP, 13-Feb-2025)

Ref Expression
Assertion oaun3lem3 ⊢A∈On∧B∈On→x|∃a∈A∃b∈Bx=a+𝑜b∈On

Proof

Step Hyp Ref Expression
1 oaun3lem1 ⊢A∈On∧B∈On→Ord⁡x|∃a∈A∃b∈Bx=a+𝑜b
2 oacl ⊢A∈On∧B∈On→A+𝑜B∈On
3 oaun3lem2 ⊢A∈On∧B∈On→x|∃a∈A∃b∈Bx=a+𝑜b⊆A+𝑜B
4 2 3 ssexd ⊢A∈On∧B∈On→x|∃a∈A∃b∈Bx=a+𝑜b∈V
5 elon2 ⊢x|∃a∈A∃b∈Bx=a+𝑜b∈On↔Ord⁡x|∃a∈A∃b∈Bx=a+𝑜b∧x|∃a∈A∃b∈Bx=a+𝑜b∈V
6 1 4 5 sylanbrc ⊢A∈On∧B∈On→x|∃a∈A∃b∈Bx=a+𝑜b∈On