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) Avoid ax-rep . (Revised by BTernaryTau, 3-Jul-2024)

Ref Expression
Assertion ficardun ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( card ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )

Proof

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