Metamath Proof Explorer

Theorem hashunx

Description: The size of the union of disjoint sets is the result of the extended real addition of their sizes, analogous to hashun . (Contributed by Alexander van der Vekens, 21-Dec-2017)

Ref Expression
Assertion hashunx ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 hashun ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
2 1 3expa ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
3 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
4 3 nn0red ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℝ )
5 hashcl ⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
6 5 nn0red ⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℝ )
7 4 6 anim12i ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ∈ ℝ ∧ ( ♯ ‘ 𝐵 ) ∈ ℝ ) )
8 7 adantr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( ♯ ‘ 𝐴 ) ∈ ℝ ∧ ( ♯ ‘ 𝐵 ) ∈ ℝ ) )
9 rexadd ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℝ ∧ ( ♯ ‘ 𝐵 ) ∈ ℝ ) → ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
10 8 9 syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
11 10 eqcomd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) )
12 2 11 eqtrd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) )
13 12 expcom ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) ) )
14 13 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) ) )
15 unexg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
16 unfir ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ Fin → ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) )
17 16 con3i ⊢ ( ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ¬ ( 𝐴 ∪ 𝐵 ) ∈ Fin )
18 hashinf ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ∈ V ∧ ¬ ( 𝐴 ∪ 𝐵 ) ∈ Fin ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = +∞ )
19 15 17 18 syl2anr ⊢ ( ( ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = +∞ )
20 ianor ⊢ ( ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ↔ ( ¬ 𝐴 ∈ Fin ∨ ¬ 𝐵 ∈ Fin ) )
21 simprl ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → 𝐴 ∈ 𝑉 )
22 simprr ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → 𝐵 ∈ 𝑊 )
23 hashnfinnn0 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ∉ ℕ0 )
24 23 ex ⊢ ( 𝐴 ∈ 𝑉 → ( ¬ 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∉ ℕ0 ) )
25 24 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ¬ 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∉ ℕ0 ) )
26 25 impcom ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ♯ ‘ 𝐴 ) ∉ ℕ0 )
27 hashinfxadd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( ♯ ‘ 𝐴 ) ∉ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) = +∞ )
28 21 22 26 27 syl3anc ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) = +∞ )
29 28 eqcomd ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → +∞ = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) )
30 29 ex ⊢ ( ¬ 𝐴 ∈ Fin → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → +∞ = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) ) )
31 hashxrcl ⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℝ* )
32 hashxrcl ⊢ ( 𝐵 ∈ 𝑊 → ( ♯ ‘ 𝐵 ) ∈ ℝ* )
33 31 32 anim12i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( ♯ ‘ 𝐴 ) ∈ ℝ* ∧ ( ♯ ‘ 𝐵 ) ∈ ℝ* ) )
34 33 adantl ⊢ ( ( ¬ 𝐵 ∈ Fin ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ( ♯ ‘ 𝐴 ) ∈ ℝ* ∧ ( ♯ ‘ 𝐵 ) ∈ ℝ* ) )
35 xaddcom ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℝ* ∧ ( ♯ ‘ 𝐵 ) ∈ ℝ* ) → ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐵 ) +𝑒 ( ♯ ‘ 𝐴 ) ) )
36 34 35 syl ⊢ ( ( ¬ 𝐵 ∈ Fin ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐵 ) +𝑒 ( ♯ ‘ 𝐴 ) ) )
37 simprr ⊢ ( ( ¬ 𝐵 ∈ Fin ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → 𝐵 ∈ 𝑊 )
38 simprl ⊢ ( ( ¬ 𝐵 ∈ Fin ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → 𝐴 ∈ 𝑉 )
39 hashnfinnn0 ⊢ ( ( 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) ∉ ℕ0 )
40 39 ex ⊢ ( 𝐵 ∈ 𝑊 → ( ¬ 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∉ ℕ0 ) )
41 40 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ¬ 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∉ ℕ0 ) )
42 41 impcom ⊢ ( ( ¬ 𝐵 ∈ Fin ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ♯ ‘ 𝐵 ) ∉ ℕ0 )
43 hashinfxadd ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ ( ♯ ‘ 𝐵 ) ∉ ℕ0 ) → ( ( ♯ ‘ 𝐵 ) +𝑒 ( ♯ ‘ 𝐴 ) ) = +∞ )
44 37 38 42 43 syl3anc ⊢ ( ( ¬ 𝐵 ∈ Fin ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ( ♯ ‘ 𝐵 ) +𝑒 ( ♯ ‘ 𝐴 ) ) = +∞ )
45 36 44 eqtrd ⊢ ( ( ¬ 𝐵 ∈ Fin ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) = +∞ )
46 45 eqcomd ⊢ ( ( ¬ 𝐵 ∈ Fin ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → +∞ = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) )
47 46 ex ⊢ ( ¬ 𝐵 ∈ Fin → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → +∞ = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) ) )
48 30 47 jaoi ⊢ ( ( ¬ 𝐴 ∈ Fin ∨ ¬ 𝐵 ∈ Fin ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → +∞ = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) ) )
49 20 48 sylbi ⊢ ( ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → +∞ = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) ) )
50 49 imp ⊢ ( ( ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → +∞ = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) )
51 19 50 eqtrd ⊢ ( ( ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) )
52 51 expcom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) ) )
53 52 3adant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ¬ ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) ) )
54 14 53 pm2.61d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ♯ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) )