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 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )

Proof

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