Metamath Proof Explorer

Theorem ficardadju

Description: The disjoint union of finite sets is equinumerous to the ordinal sum of the cardinalities of those sets. (Contributed by BTernaryTau, 3-Jul-2024)

Ref Expression
Assertion ficardadju ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ficardom ⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω )
2 ficardom ⊢ ( 𝐵 ∈ Fin → ( card ‘ 𝐵 ) ∈ ω )
3 nnadju ⊢ ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ 𝐵 ) ∈ ω ) → ( card ‘ ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) ) = ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )
4 df-dju ⊢ ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) = ( ( { ∅ } × ( card ‘ 𝐴 ) ) ∪ ( { 1o } × ( card ‘ 𝐵 ) ) )
5 snfi ⊢ { ∅ } ∈ Fin
6 nnfi ⊢ ( ( card ‘ 𝐴 ) ∈ ω → ( card ‘ 𝐴 ) ∈ Fin )
7 xpfi ⊢ ( ( { ∅ } ∈ Fin ∧ ( card ‘ 𝐴 ) ∈ Fin ) → ( { ∅ } × ( card ‘ 𝐴 ) ) ∈ Fin )
8 5 6 7 sylancr ⊢ ( ( card ‘ 𝐴 ) ∈ ω → ( { ∅ } × ( card ‘ 𝐴 ) ) ∈ Fin )
9 snfi ⊢ { 1o } ∈ Fin
10 nnfi ⊢ ( ( card ‘ 𝐵 ) ∈ ω → ( card ‘ 𝐵 ) ∈ Fin )
11 xpfi ⊢ ( ( { 1o } ∈ Fin ∧ ( card ‘ 𝐵 ) ∈ Fin ) → ( { 1o } × ( card ‘ 𝐵 ) ) ∈ Fin )
12 9 10 11 sylancr ⊢ ( ( card ‘ 𝐵 ) ∈ ω → ( { 1o } × ( card ‘ 𝐵 ) ) ∈ Fin )
13 unfi ⊢ ( ( ( { ∅ } × ( card ‘ 𝐴 ) ) ∈ Fin ∧ ( { 1o } × ( card ‘ 𝐵 ) ) ∈ Fin ) → ( ( { ∅ } × ( card ‘ 𝐴 ) ) ∪ ( { 1o } × ( card ‘ 𝐵 ) ) ) ∈ Fin )
14 8 12 13 syl2an ⊢ ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ 𝐵 ) ∈ ω ) → ( ( { ∅ } × ( card ‘ 𝐴 ) ) ∪ ( { 1o } × ( card ‘ 𝐵 ) ) ) ∈ Fin )
15 4 14 eqeltrid ⊢ ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ 𝐵 ) ∈ ω ) → ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) ∈ Fin )
16 ficardid ⊢ ( ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) ∈ Fin → ( card ‘ ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) ) ≈ ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) )
17 15 16 syl ⊢ ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ 𝐵 ) ∈ ω ) → ( card ‘ ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) ) ≈ ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) )
18 3 17 eqbrtrrd ⊢ ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ 𝐵 ) ∈ ω ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) )
19 1 2 18 syl2an ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) )
20 ficardid ⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ≈ 𝐴 )
21 ficardid ⊢ ( 𝐵 ∈ Fin → ( card ‘ 𝐵 ) ≈ 𝐵 )
22 djuen ⊢ ( ( ( card ‘ 𝐴 ) ≈ 𝐴 ∧ ( card ‘ 𝐵 ) ≈ 𝐵 ) → ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) ≈ ( 𝐴 ⊔ 𝐵 ) )
23 20 21 22 syl2an ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) ≈ ( 𝐴 ⊔ 𝐵 ) )
24 entr ⊢ ( ( ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) ∧ ( ( card ‘ 𝐴 ) ⊔ ( card ‘ 𝐵 ) ) ≈ ( 𝐴 ⊔ 𝐵 ) ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( 𝐴 ⊔ 𝐵 ) )
25 19 23 24 syl2anc ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( 𝐴 ⊔ 𝐵 ) )
26 25 ensymd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )