Metamath Proof Explorer

Theorem ficardadju

Description: The disjoint union of finite sets is equinumerous to the ordinal sum of the cardinalities of those sets. (Contributed by BTernaryTau, 3-Jul-2024)

Ref Expression
Assertion ficardadju ⊢ A ∈ Fin ∧ B ∈ Fin → A ⊔︀ B ≈ card ⁡ A + 𝑜 card ⁡ B

Proof

Step Hyp Ref Expression
1 ficardom ⊢ A ∈ Fin → card ⁡ A ∈ ω
2 ficardom ⊢ B ∈ Fin → card ⁡ B ∈ ω
3 nnadju ⊢ card ⁡ A ∈ ω ∧ card ⁡ B ∈ ω → card ⁡ card ⁡ A ⊔︀ card ⁡ B = card ⁡ A + 𝑜 card ⁡ B
4 df-dju ⊢ card ⁡ A ⊔︀ card ⁡ B = ∅ × card ⁡ A ∪ 1 𝑜 × card ⁡ B
5 snfi ⊢ ∅ ∈ Fin
6 nnfi ⊢ card ⁡ A ∈ ω → card ⁡ A ∈ Fin
7 xpfi ⊢ ∅ ∈ Fin ∧ card ⁡ A ∈ Fin → ∅ × card ⁡ A ∈ Fin
8 5 6 7 sylancr ⊢ card ⁡ A ∈ ω → ∅ × card ⁡ A ∈ Fin
9 snfi ⊢ 1 𝑜 ∈ Fin
10 nnfi ⊢ card ⁡ B ∈ ω → card ⁡ B ∈ Fin
11 xpfi ⊢ 1 𝑜 ∈ Fin ∧ card ⁡ B ∈ Fin → 1 𝑜 × card ⁡ B ∈ Fin
12 9 10 11 sylancr ⊢ card ⁡ B ∈ ω → 1 𝑜 × card ⁡ B ∈ Fin
13 unfi ⊢ ∅ × card ⁡ A ∈ Fin ∧ 1 𝑜 × card ⁡ B ∈ Fin → ∅ × card ⁡ A ∪ 1 𝑜 × card ⁡ B ∈ Fin
14 8 12 13 syl2an ⊢ card ⁡ A ∈ ω ∧ card ⁡ B ∈ ω → ∅ × card ⁡ A ∪ 1 𝑜 × card ⁡ B ∈ Fin
15 4 14 eqeltrid ⊢ card ⁡ A ∈ ω ∧ card ⁡ B ∈ ω → card ⁡ A ⊔︀ card ⁡ B ∈ Fin
16 ficardid ⊢ card ⁡ A ⊔︀ card ⁡ B ∈ Fin → card ⁡ card ⁡ A ⊔︀ card ⁡ B ≈ card ⁡ A ⊔︀ card ⁡ B
17 15 16 syl ⊢ card ⁡ A ∈ ω ∧ card ⁡ B ∈ ω → card ⁡ card ⁡ A ⊔︀ card ⁡ B ≈ card ⁡ A ⊔︀ card ⁡ B
18 3 17 eqbrtrrd ⊢ card ⁡ A ∈ ω ∧ card ⁡ B ∈ ω → card ⁡ A + 𝑜 card ⁡ B ≈ card ⁡ A ⊔︀ card ⁡ B
19 1 2 18 syl2an ⊢ A ∈ Fin ∧ B ∈ Fin → card ⁡ A + 𝑜 card ⁡ B ≈ card ⁡ A ⊔︀ card ⁡ B
20 ficardid ⊢ A ∈ Fin → card ⁡ A ≈ A
21 ficardid ⊢ B ∈ Fin → card ⁡ B ≈ B
22 djuen ⊢ card ⁡ A ≈ A ∧ card ⁡ B ≈ B → card ⁡ A ⊔︀ card ⁡ B ≈ A ⊔︀ B
23 20 21 22 syl2an ⊢ A ∈ Fin ∧ B ∈ Fin → card ⁡ A ⊔︀ card ⁡ B ≈ A ⊔︀ B
24 entr ⊢ card ⁡ A + 𝑜 card ⁡ B ≈ card ⁡ A ⊔︀ card ⁡ B ∧ card ⁡ A ⊔︀ card ⁡ B ≈ A ⊔︀ B → card ⁡ A + 𝑜 card ⁡ B ≈ A ⊔︀ B
25 19 23 24 syl2anc ⊢ A ∈ Fin ∧ B ∈ Fin → card ⁡ A + 𝑜 card ⁡ B ≈ A ⊔︀ B
26 25 ensymd ⊢ A ∈ Fin ∧ B ∈ Fin → A ⊔︀ B ≈ card ⁡ A + 𝑜 card ⁡ B