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)

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

Proof

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