Metamath Proof Explorer

Theorem ficardun2OLD

Description: Obsolete version of ficardun2 as of 3-Jul-2024. (Contributed by Mario Carneiro, 5-Feb-2013) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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