Metamath Proof Explorer

Theorem ficardun

Description: The cardinality of the union of disjoint, finite sets is the ordinal sum of their cardinalities. (Contributed by Paul Chapman, 5-Jun-2009) (Proof shortened by Mario Carneiro, 28-Apr-2015) Avoid ax-rep . (Revised by BTernaryTau, 3-Jul-2024)

Ref Expression
Assertion ficardun ⊢ A ∈ Fin ∧ B ∈ Fin ∧ A ∩ B = ∅ → card ⁡ A ∪ B = card ⁡ A + 𝑜 card ⁡ B

Proof

Step Hyp Ref Expression
1 ficardadju ⊢ A ∈ Fin ∧ B ∈ Fin → A ⊔︀ B ≈ card ⁡ A + 𝑜 card ⁡ B
2 1 3adant3 ⊢ A ∈ Fin ∧ B ∈ Fin ∧ A ∩ B = ∅ → A ⊔︀ B ≈ card ⁡ A + 𝑜 card ⁡ B
3 2 ensymd ⊢ A ∈ Fin ∧ B ∈ Fin ∧ A ∩ B = ∅ → card ⁡ A + 𝑜 card ⁡ B ≈ A ⊔︀ B
4 endjudisj ⊢ A ∈ Fin ∧ B ∈ Fin ∧ A ∩ B = ∅ → A ⊔︀ B ≈ A ∪ B
5 entr ⊢ card ⁡ A + 𝑜 card ⁡ B ≈ A ⊔︀ B ∧ A ⊔︀ B ≈ A ∪ B → card ⁡ A + 𝑜 card ⁡ B ≈ A ∪ B
6 3 4 5 syl2anc ⊢ A ∈ Fin ∧ B ∈ Fin ∧ A ∩ B = ∅ → card ⁡ A + 𝑜 card ⁡ B ≈ A ∪ B
7 carden2b ⊢ card ⁡ A + 𝑜 card ⁡ B ≈ A ∪ B → card ⁡ card ⁡ A + 𝑜 card ⁡ B = card ⁡ A ∪ B
8 6 7 syl ⊢ A ∈ Fin ∧ B ∈ Fin ∧ A ∩ B = ∅ → card ⁡ card ⁡ A + 𝑜 card ⁡ B = card ⁡ A ∪ B
9 ficardom ⊢ A ∈ Fin → card ⁡ A ∈ ω
10 ficardom ⊢ B ∈ Fin → card ⁡ B ∈ ω
11 nnacl ⊢ card ⁡ A ∈ ω ∧ card ⁡ B ∈ ω → card ⁡ A + 𝑜 card ⁡ B ∈ ω
12 cardnn ⊢ card ⁡ A + 𝑜 card ⁡ B ∈ ω → card ⁡ card ⁡ A + 𝑜 card ⁡ B = card ⁡ A + 𝑜 card ⁡ B
13 11 12 syl ⊢ card ⁡ A ∈ ω ∧ card ⁡ B ∈ ω → card ⁡ card ⁡ A + 𝑜 card ⁡ B = card ⁡ A + 𝑜 card ⁡ B
14 9 10 13 syl2an ⊢ A ∈ Fin ∧ B ∈ Fin → card ⁡ card ⁡ A + 𝑜 card ⁡ B = card ⁡ A + 𝑜 card ⁡ B
15 14 3adant3 ⊢ A ∈ Fin ∧ B ∈ Fin ∧ A ∩ B = ∅ → card ⁡ card ⁡ A + 𝑜 card ⁡ B = card ⁡ A + 𝑜 card ⁡ B
16 8 15 eqtr3d ⊢ A ∈ Fin ∧ B ∈ Fin ∧ A ∩ B = ∅ → card ⁡ A ∪ B = card ⁡ A + 𝑜 card ⁡ B