Metamath Proof Explorer

Theorem ficardun2OLD

Description: Obsolete version of ficardun2 as of 3-Jul-2024. (Contributed by Mario Carneiro, 5-Feb-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ficardun2OLD ⊢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 finnum ⊢A∈Fin→A∈dom⁡card
3 finnum ⊢B∈Fin→B∈dom⁡card
4 cardadju ⊢A∈dom⁡card∧B∈dom⁡card→A⊔︀B≈card⁡A+𝑜card⁡B
5 2 3 4 syl2an ⊢A∈Fin∧B∈Fin→A⊔︀B≈card⁡A+𝑜card⁡B
6 domentr ⊢A∪B≼A⊔︀B∧A⊔︀B≈card⁡A+𝑜card⁡B→A∪B≼card⁡A+𝑜card⁡B
7 1 5 6 syl2anc ⊢A∈Fin∧B∈Fin→A∪B≼card⁡A+𝑜card⁡B
8 unfi ⊢A∈Fin∧B∈Fin→A∪B∈Fin
9 finnum ⊢A∪B∈Fin→A∪B∈dom⁡card
10 8 9 syl ⊢A∈Fin∧B∈Fin→A∪B∈dom⁡card
11 ficardom ⊢A∈Fin→card⁡A∈ω
12 ficardom ⊢B∈Fin→card⁡B∈ω
13 nnacl ⊢card⁡A∈ω∧card⁡B∈ω→card⁡A+𝑜card⁡B∈ω
14 11 12 13 syl2an ⊢A∈Fin∧B∈Fin→card⁡A+𝑜card⁡B∈ω
15 nnon ⊢card⁡A+𝑜card⁡B∈ω→card⁡A+𝑜card⁡B∈On
16 onenon ⊢card⁡A+𝑜card⁡B∈On→card⁡A+𝑜card⁡B∈dom⁡card
17 14 15 16 3syl ⊢A∈Fin∧B∈Fin→card⁡A+𝑜card⁡B∈dom⁡card
18 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
19 10 17 18 syl2anc ⊢A∈Fin∧B∈Fin→card⁡A∪B⊆card⁡card⁡A+𝑜card⁡B↔A∪B≼card⁡A+𝑜card⁡B
20 7 19 mpbird ⊢A∈Fin∧B∈Fin→card⁡A∪B⊆card⁡card⁡A+𝑜card⁡B
21 cardnn ⊢card⁡A+𝑜card⁡B∈ω→card⁡card⁡A+𝑜card⁡B=card⁡A+𝑜card⁡B
22 14 21 syl ⊢A∈Fin∧B∈Fin→card⁡card⁡A+𝑜card⁡B=card⁡A+𝑜card⁡B
23 20 22 sseqtrd ⊢A∈Fin∧B∈Fin→card⁡A∪B⊆card⁡A+𝑜card⁡B