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 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )

Proof

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