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 ⊢ A ∈ Fin ∧ B ∈ Fin → card ⁡ A ∪ B ⊆ card ⁡ A + 𝑜 card ⁡ B

Proof

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