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