Metamath Proof Explorer

Theorem hashun2

Description: The size of the union of finite sets is less than or equal to the sum of their sizes. (Contributed by Mario Carneiro, 23-Sep-2013) (Proof shortened by Mario Carneiro, 27-Jul-2014)

Ref Expression
Assertion hashun2 ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ≤ A + B

Proof

Step Hyp Ref Expression
1 undif2 ⊢ A ∪ B ∖ A = A ∪ B
2 1 fveq2i ⊢ A ∪ B ∖ A = A ∪ B
3 diffi ⊢ B ∈ Fin → B ∖ A ∈ Fin
4 disjdif ⊢ A ∩ B ∖ A = ∅
5 hashun ⊢ A ∈ Fin ∧ B ∖ A ∈ Fin ∧ A ∩ B ∖ A = ∅ → A ∪ B ∖ A = A + B ∖ A
6 4 5 mp3an3 ⊢ A ∈ Fin ∧ B ∖ A ∈ Fin → A ∪ B ∖ A = A + B ∖ A
7 3 6 sylan2 ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ∖ A = A + B ∖ A
8 2 7 eqtr3id ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B = A + B ∖ A
9 3 adantl ⊢ A ∈ Fin ∧ B ∈ Fin → B ∖ A ∈ Fin
10 hashcl ⊢ B ∖ A ∈ Fin → B ∖ A ∈ ℕ 0
11 9 10 syl ⊢ A ∈ Fin ∧ B ∈ Fin → B ∖ A ∈ ℕ 0
12 11 nn0red ⊢ A ∈ Fin ∧ B ∈ Fin → B ∖ A ∈ ℝ
13 hashcl ⊢ B ∈ Fin → B ∈ ℕ 0
14 13 adantl ⊢ A ∈ Fin ∧ B ∈ Fin → B ∈ ℕ 0
15 14 nn0red ⊢ A ∈ Fin ∧ B ∈ Fin → B ∈ ℝ
16 hashcl ⊢ A ∈ Fin → A ∈ ℕ 0
17 16 adantr ⊢ A ∈ Fin ∧ B ∈ Fin → A ∈ ℕ 0
18 17 nn0red ⊢ A ∈ Fin ∧ B ∈ Fin → A ∈ ℝ
19 simpr ⊢ A ∈ Fin ∧ B ∈ Fin → B ∈ Fin
20 difss ⊢ B ∖ A ⊆ B
21 ssdomg ⊢ B ∈ Fin → B ∖ A ⊆ B → B ∖ A ≼ B
22 19 20 21 mpisyl ⊢ A ∈ Fin ∧ B ∈ Fin → B ∖ A ≼ B
23 hashdom ⊢ B ∖ A ∈ Fin ∧ B ∈ Fin → B ∖ A ≤ B ↔ B ∖ A ≼ B
24 9 23 sylancom ⊢ A ∈ Fin ∧ B ∈ Fin → B ∖ A ≤ B ↔ B ∖ A ≼ B
25 22 24 mpbird ⊢ A ∈ Fin ∧ B ∈ Fin → B ∖ A ≤ B
26 12 15 18 25 leadd2dd ⊢ A ∈ Fin ∧ B ∈ Fin → A + B ∖ A ≤ A + B
27 8 26 eqbrtrd ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ≤ A + B