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 ∈ B x = a + 𝑜 b ∈ On

Proof

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