Metamath Proof Explorer

Theorem ficardunOLD

Description: Obsolete version of ficardun as of 3-Jul-2024. (Contributed by Paul Chapman, 5-Jun-2009) (Proof shortened by Mario Carneiro, 28-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ficardunOLD ⊢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