Metamath Proof Explorer

Theorem oaun3lem4

Description: The class of all ordinal sums of elements from two ordinals is less than the successor to the sum. Lemma for oaun3 . (Contributed by RP, 12-Feb-2025)

Ref Expression
Assertion oaun3lem4 ⊢ A ∈ On ∧ B ∈ On → x | ∃ a ∈ A ∃ b ∈ B x = a + 𝑜 b ∈ suc ⁡ A + 𝑜 B

Proof

Step Hyp Ref Expression
1 oaun3lem2 ⊢ A ∈ On ∧ B ∈ On → x | ∃ a ∈ A ∃ b ∈ B x = a + 𝑜 b ⊆ A + 𝑜 B
2 oaun3lem3 ⊢ A ∈ On ∧ B ∈ On → x | ∃ a ∈ A ∃ b ∈ B x = a + 𝑜 b ∈ On
3 oacl ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B ∈ On
4 onsssuc ⊢ x | ∃ a ∈ A ∃ b ∈ B x = a + 𝑜 b ∈ On ∧ A + 𝑜 B ∈ On → x | ∃ a ∈ A ∃ b ∈ B x = a + 𝑜 b ⊆ A + 𝑜 B ↔ x | ∃ a ∈ A ∃ b ∈ B x = a + 𝑜 b ∈ suc ⁡ A + 𝑜 B
5 2 3 4 syl2anc ⊢ A ∈ On ∧ B ∈ On → x | ∃ a ∈ A ∃ b ∈ B x = a + 𝑜 b ⊆ A + 𝑜 B ↔ x | ∃ a ∈ A ∃ b ∈ B x = a + 𝑜 b ∈ suc ⁡ A + 𝑜 B
6 1 5 mpbid ⊢ A ∈ On ∧ B ∈ On → x | ∃ a ∈ A ∃ b ∈ B x = a + 𝑜 b ∈ suc ⁡ A + 𝑜 B