Metamath Proof Explorer

Theorem ficardun2

Description: The cardinality of the union of finite sets is at most the ordinal sum of their cardinalities. (Contributed by Mario Carneiro, 5-Feb-2013) Avoid ax-rep . (Revised by BTernaryTau, 3-Jul-2024)

Ref Expression
Assertion ficardun2 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( card ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 undjudom ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐵 ) )
2 ficardadju ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )
3 domentr ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐵 ) ∧ ( 𝐴 ⊔ 𝐵 ) ≈ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) → ( 𝐴 ∪ 𝐵 ) ≼ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )
4 1 2 3 syl2anc ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∪ 𝐵 ) ≼ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )
5 unfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin )
6 finnum ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ Fin → ( 𝐴 ∪ 𝐵 ) ∈ dom card )
7 5 6 syl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∪ 𝐵 ) ∈ dom card )
8 ficardom ⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω )
9 ficardom ⊢ ( 𝐵 ∈ Fin → ( card ‘ 𝐵 ) ∈ ω )
10 nnacl ⊢ ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ 𝐵 ) ∈ ω ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ ω )
11 8 9 10 syl2an ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ ω )
12 nnon ⊢ ( ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ ω → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ On )
13 onenon ⊢ ( ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ On → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ dom card )
14 11 12 13 3syl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ dom card )
15 carddom2 ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ∈ dom card ∧ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ dom card ) → ( ( card ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( card ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) ↔ ( 𝐴 ∪ 𝐵 ) ≼ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) )
16 7 14 15 syl2anc ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( card ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( card ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) ↔ ( 𝐴 ∪ 𝐵 ) ≼ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) )
17 4 16 mpbird ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( card ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( card ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) )
18 cardnn ⊢ ( ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ ω → ( card ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) = ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )
19 11 18 syl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( card ‘ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ) = ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )
20 17 19 sseqtrd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( card ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )