Metamath Proof Explorer

Theorem onadju

Description: The cardinal and ordinal sums are always equinumerous. (Contributed by Mario Carneiro, 6-Feb-2013) (Revised by Jim Kingdon, 7-Sep-2023)

Ref Expression
Assertion onadju ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B ≈ A ⊔︀ B

Proof

Step Hyp Ref Expression
1 enrefg ⊢ A ∈ On → A ≈ A
2 1 adantr ⊢ A ∈ On ∧ B ∈ On → A ≈ A
3 simpr ⊢ A ∈ On ∧ B ∈ On → B ∈ On
4 eqid ⊢ x ∈ B ⟼ A + 𝑜 x = x ∈ B ⟼ A + 𝑜 x
5 4 oacomf1olem ⊢ B ∈ On ∧ A ∈ On → x ∈ B ⟼ A + 𝑜 x : B ⟶ 1-1 onto ran ⁡ x ∈ B ⟼ A + 𝑜 x ∧ ran ⁡ x ∈ B ⟼ A + 𝑜 x ∩ A = ∅
6 5 ancoms ⊢ A ∈ On ∧ B ∈ On → x ∈ B ⟼ A + 𝑜 x : B ⟶ 1-1 onto ran ⁡ x ∈ B ⟼ A + 𝑜 x ∧ ran ⁡ x ∈ B ⟼ A + 𝑜 x ∩ A = ∅
7 6 simpld ⊢ A ∈ On ∧ B ∈ On → x ∈ B ⟼ A + 𝑜 x : B ⟶ 1-1 onto ran ⁡ x ∈ B ⟼ A + 𝑜 x
8 f1oeng ⊢ B ∈ On ∧ x ∈ B ⟼ A + 𝑜 x : B ⟶ 1-1 onto ran ⁡ x ∈ B ⟼ A + 𝑜 x → B ≈ ran ⁡ x ∈ B ⟼ A + 𝑜 x
9 3 7 8 syl2anc ⊢ A ∈ On ∧ B ∈ On → B ≈ ran ⁡ x ∈ B ⟼ A + 𝑜 x
10 incom ⊢ A ∩ ran ⁡ x ∈ B ⟼ A + 𝑜 x = ran ⁡ x ∈ B ⟼ A + 𝑜 x ∩ A
11 6 simprd ⊢ A ∈ On ∧ B ∈ On → ran ⁡ x ∈ B ⟼ A + 𝑜 x ∩ A = ∅
12 10 11 syl5eq ⊢ A ∈ On ∧ B ∈ On → A ∩ ran ⁡ x ∈ B ⟼ A + 𝑜 x = ∅
13 djuenun ⊢ A ≈ A ∧ B ≈ ran ⁡ x ∈ B ⟼ A + 𝑜 x ∧ A ∩ ran ⁡ x ∈ B ⟼ A + 𝑜 x = ∅ → A ⊔︀ B ≈ A ∪ ran ⁡ x ∈ B ⟼ A + 𝑜 x
14 2 9 12 13 syl3anc ⊢ A ∈ On ∧ B ∈ On → A ⊔︀ B ≈ A ∪ ran ⁡ x ∈ B ⟼ A + 𝑜 x
15 oarec ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B = A ∪ ran ⁡ x ∈ B ⟼ A + 𝑜 x
16 14 15 breqtrrd ⊢ A ∈ On ∧ B ∈ On → A ⊔︀ B ≈ A + 𝑜 B
17 16 ensymd ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B ≈ A ⊔︀ B