Metamath Proof Explorer

Theorem ficardun2

Description: The cardinality of the union of finite sets is at most the ordinal sum of their cardinalities. (Contributed by Mario Carneiro, 5-Feb-2013) Avoid ax-rep . (Revised by BTernaryTau, 3-Jul-2024)

Ref Expression
Assertion ficardun2 ⊢ A ∈ Fin ∧ B ∈ Fin → card ⁡ A ∪ B ⊆ card ⁡ A + 𝑜 card ⁡ B

Proof

Step Hyp Ref Expression
1 undjudom ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ≼ A ⊔︀ B
2 ficardadju ⊢ A ∈ Fin ∧ B ∈ Fin → A ⊔︀ B ≈ card ⁡ A + 𝑜 card ⁡ B
3 domentr ⊢ A ∪ B ≼ A ⊔︀ B ∧ A ⊔︀ B ≈ card ⁡ A + 𝑜 card ⁡ B → A ∪ B ≼ card ⁡ A + 𝑜 card ⁡ B
4 1 2 3 syl2anc ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ≼ card ⁡ A + 𝑜 card ⁡ B
5 unfi ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ∈ Fin
6 finnum ⊢ A ∪ B ∈ Fin → A ∪ B ∈ dom ⁡ card
7 5 6 syl ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ∈ dom ⁡ card
8 ficardom ⊢ A ∈ Fin → card ⁡ A ∈ ω
9 ficardom ⊢ B ∈ Fin → card ⁡ B ∈ ω
10 nnacl ⊢ card ⁡ A ∈ ω ∧ card ⁡ B ∈ ω → card ⁡ A + 𝑜 card ⁡ B ∈ ω
11 8 9 10 syl2an ⊢ A ∈ Fin ∧ B ∈ Fin → card ⁡ A + 𝑜 card ⁡ B ∈ ω
12 nnon ⊢ card ⁡ A + 𝑜 card ⁡ B ∈ ω → card ⁡ A + 𝑜 card ⁡ B ∈ On
13 onenon ⊢ card ⁡ A + 𝑜 card ⁡ B ∈ On → card ⁡ A + 𝑜 card ⁡ B ∈ dom ⁡ card
14 11 12 13 3syl ⊢ A ∈ Fin ∧ B ∈ Fin → card ⁡ A + 𝑜 card ⁡ B ∈ dom ⁡ card
15 carddom2 ⊢ A ∪ B ∈ dom ⁡ card ∧ card ⁡ A + 𝑜 card ⁡ B ∈ dom ⁡ card → card ⁡ A ∪ B ⊆ card ⁡ card ⁡ A + 𝑜 card ⁡ B ↔ A ∪ B ≼ card ⁡ A + 𝑜 card ⁡ B
16 7 14 15 syl2anc ⊢ A ∈ Fin ∧ B ∈ Fin → card ⁡ A ∪ B ⊆ card ⁡ card ⁡ A + 𝑜 card ⁡ B ↔ A ∪ B ≼ card ⁡ A + 𝑜 card ⁡ B
17 4 16 mpbird ⊢ A ∈ Fin ∧ B ∈ Fin → card ⁡ A ∪ B ⊆ card ⁡ card ⁡ A + 𝑜 card ⁡ B
18 cardnn ⊢ card ⁡ A + 𝑜 card ⁡ B ∈ ω → card ⁡ card ⁡ A + 𝑜 card ⁡ B = card ⁡ A + 𝑜 card ⁡ B
19 11 18 syl ⊢ A ∈ Fin ∧ B ∈ Fin → card ⁡ card ⁡ A + 𝑜 card ⁡ B = card ⁡ A + 𝑜 card ⁡ B
20 17 19 sseqtrd ⊢ A ∈ Fin ∧ B ∈ Fin → card ⁡ A ∪ B ⊆ card ⁡ A + 𝑜 card ⁡ B