Metamath Proof Explorer

Theorem oaun2

Description: Ordinal addition as a union of classes. (Contributed by RP, 13-Feb-2025)

Ref Expression
Assertion oaun2 ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B = ⋃ x | ∃ a ∈ A x = a y | ∃ b ∈ B y = A + 𝑜 b

Proof

Step Hyp Ref Expression
1 oacl ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B ∈ On
2 1 difexd ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B ∖ A ∈ V
3 uniprg ⊢ A ∈ On ∧ A + 𝑜 B ∖ A ∈ V → ⋃ A A + 𝑜 B ∖ A = A ∪ A + 𝑜 B ∖ A
4 2 3 syldan ⊢ A ∈ On ∧ B ∈ On → ⋃ A A + 𝑜 B ∖ A = A ∪ A + 𝑜 B ∖ A
5 rp-abid ⊢ A = x | ∃ a ∈ A x = a
6 5 a1i ⊢ A ∈ On ∧ B ∈ On → A = x | ∃ a ∈ A x = a
7 oadif1 ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B ∖ A = y | ∃ b ∈ B y = A + 𝑜 b
8 6 7 preq12d ⊢ A ∈ On ∧ B ∈ On → A A + 𝑜 B ∖ A = x | ∃ a ∈ A x = a y | ∃ b ∈ B y = A + 𝑜 b
9 8 unieqd ⊢ A ∈ On ∧ B ∈ On → ⋃ A A + 𝑜 B ∖ A = ⋃ x | ∃ a ∈ A x = a y | ∃ b ∈ B y = A + 𝑜 b
10 undif2 ⊢ A ∪ A + 𝑜 B ∖ A = A ∪ A + 𝑜 B
11 oaword1 ⊢ A ∈ On ∧ B ∈ On → A ⊆ A + 𝑜 B
12 ssequn1 ⊢ A ⊆ A + 𝑜 B ↔ A ∪ A + 𝑜 B = A + 𝑜 B
13 11 12 sylib ⊢ A ∈ On ∧ B ∈ On → A ∪ A + 𝑜 B = A + 𝑜 B
14 10 13 eqtrid ⊢ A ∈ On ∧ B ∈ On → A ∪ A + 𝑜 B ∖ A = A + 𝑜 B
15 4 9 14 3eqtr3rd ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B = ⋃ x | ∃ a ∈ A x = a y | ∃ b ∈ B y = A + 𝑜 b