# 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 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\cap {B}=\varnothing \right)\to \left|{A}\cup {B}\right|=\left|{A}\right|{+}_{𝑒}\left|{B}\right|$

### Proof

Step Hyp Ref Expression
1 hashun ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\wedge {A}\cap {B}=\varnothing \right)\to \left|{A}\cup {B}\right|=\left|{A}\right|+\left|{B}\right|$
2 1 3expa ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left|{A}\cup {B}\right|=\left|{A}\right|+\left|{B}\right|$
3 hashcl ${⊢}{A}\in \mathrm{Fin}\to \left|{A}\right|\in {ℕ}_{0}$
4 3 nn0red ${⊢}{A}\in \mathrm{Fin}\to \left|{A}\right|\in ℝ$
5 hashcl ${⊢}{B}\in \mathrm{Fin}\to \left|{B}\right|\in {ℕ}_{0}$
6 5 nn0red ${⊢}{B}\in \mathrm{Fin}\to \left|{B}\right|\in ℝ$
7 4 6 anim12i ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left(\left|{A}\right|\in ℝ\wedge \left|{B}\right|\in ℝ\right)$
8 7 adantr ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left(\left|{A}\right|\in ℝ\wedge \left|{B}\right|\in ℝ\right)$
9 rexadd ${⊢}\left(\left|{A}\right|\in ℝ\wedge \left|{B}\right|\in ℝ\right)\to \left|{A}\right|{+}_{𝑒}\left|{B}\right|=\left|{A}\right|+\left|{B}\right|$
10 8 9 syl ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left|{A}\right|{+}_{𝑒}\left|{B}\right|=\left|{A}\right|+\left|{B}\right|$
11 10 eqcomd ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left|{A}\right|+\left|{B}\right|=\left|{A}\right|{+}_{𝑒}\left|{B}\right|$
12 2 11 eqtrd ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left|{A}\cup {B}\right|=\left|{A}\right|{+}_{𝑒}\left|{B}\right|$
13 12 expcom ${⊢}{A}\cap {B}=\varnothing \to \left(\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left|{A}\cup {B}\right|=\left|{A}\right|{+}_{𝑒}\left|{B}\right|\right)$
14 13 3ad2ant3 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\cap {B}=\varnothing \right)\to \left(\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left|{A}\cup {B}\right|=\left|{A}\right|{+}_{𝑒}\left|{B}\right|\right)$
15 unexg ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to {A}\cup {B}\in \mathrm{V}$
16 unfir ${⊢}{A}\cup {B}\in \mathrm{Fin}\to \left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)$
17 16 con3i ${⊢}¬\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to ¬{A}\cup {B}\in \mathrm{Fin}$
18 hashinf ${⊢}\left({A}\cup {B}\in \mathrm{V}\wedge ¬{A}\cup {B}\in \mathrm{Fin}\right)\to \left|{A}\cup {B}\right|=\mathrm{+\infty }$
19 15 17 18 syl2anr ${⊢}\left(¬\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\wedge \left({A}\in {V}\wedge {B}\in {W}\right)\right)\to \left|{A}\cup {B}\right|=\mathrm{+\infty }$
20 ianor ${⊢}¬\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)↔\left(¬{A}\in \mathrm{Fin}\vee ¬{B}\in \mathrm{Fin}\right)$
21 simprl ${⊢}\left(¬{A}\in \mathrm{Fin}\wedge \left({A}\in {V}\wedge {B}\in {W}\right)\right)\to {A}\in {V}$
22 simprr ${⊢}\left(¬{A}\in \mathrm{Fin}\wedge \left({A}\in {V}\wedge {B}\in {W}\right)\right)\to {B}\in {W}$
23 hashnfinnn0 ${⊢}\left({A}\in {V}\wedge ¬{A}\in \mathrm{Fin}\right)\to \left|{A}\right|\notin {ℕ}_{0}$
24 23 ex ${⊢}{A}\in {V}\to \left(¬{A}\in \mathrm{Fin}\to \left|{A}\right|\notin {ℕ}_{0}\right)$
25 24 adantr ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(¬{A}\in \mathrm{Fin}\to \left|{A}\right|\notin {ℕ}_{0}\right)$
26 25 impcom ${⊢}\left(¬{A}\in \mathrm{Fin}\wedge \left({A}\in {V}\wedge {B}\in {W}\right)\right)\to \left|{A}\right|\notin {ℕ}_{0}$
27 hashinfxadd ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge \left|{A}\right|\notin {ℕ}_{0}\right)\to \left|{A}\right|{+}_{𝑒}\left|{B}\right|=\mathrm{+\infty }$
28 21 22 26 27 syl3anc ${⊢}\left(¬{A}\in \mathrm{Fin}\wedge \left({A}\in {V}\wedge {B}\in {W}\right)\right)\to \left|{A}\right|{+}_{𝑒}\left|{B}\right|=\mathrm{+\infty }$
29 28 eqcomd ${⊢}\left(¬{A}\in \mathrm{Fin}\wedge \left({A}\in {V}\wedge {B}\in {W}\right)\right)\to \mathrm{+\infty }=\left|{A}\right|{+}_{𝑒}\left|{B}\right|$
30 29 ex ${⊢}¬{A}\in \mathrm{Fin}\to \left(\left({A}\in {V}\wedge {B}\in {W}\right)\to \mathrm{+\infty }=\left|{A}\right|{+}_{𝑒}\left|{B}\right|\right)$
31 hashxrcl ${⊢}{A}\in {V}\to \left|{A}\right|\in {ℝ}^{*}$
32 hashxrcl ${⊢}{B}\in {W}\to \left|{B}\right|\in {ℝ}^{*}$
33 31 32 anim12i ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left|{A}\right|\in {ℝ}^{*}\wedge \left|{B}\right|\in {ℝ}^{*}\right)$
34 33 adantl ${⊢}\left(¬{B}\in \mathrm{Fin}\wedge \left({A}\in {V}\wedge {B}\in {W}\right)\right)\to \left(\left|{A}\right|\in {ℝ}^{*}\wedge \left|{B}\right|\in {ℝ}^{*}\right)$
35 xaddcom ${⊢}\left(\left|{A}\right|\in {ℝ}^{*}\wedge \left|{B}\right|\in {ℝ}^{*}\right)\to \left|{A}\right|{+}_{𝑒}\left|{B}\right|=\left|{B}\right|{+}_{𝑒}\left|{A}\right|$
36 34 35 syl ${⊢}\left(¬{B}\in \mathrm{Fin}\wedge \left({A}\in {V}\wedge {B}\in {W}\right)\right)\to \left|{A}\right|{+}_{𝑒}\left|{B}\right|=\left|{B}\right|{+}_{𝑒}\left|{A}\right|$
37 simprr ${⊢}\left(¬{B}\in \mathrm{Fin}\wedge \left({A}\in {V}\wedge {B}\in {W}\right)\right)\to {B}\in {W}$
38 simprl ${⊢}\left(¬{B}\in \mathrm{Fin}\wedge \left({A}\in {V}\wedge {B}\in {W}\right)\right)\to {A}\in {V}$
39 hashnfinnn0 ${⊢}\left({B}\in {W}\wedge ¬{B}\in \mathrm{Fin}\right)\to \left|{B}\right|\notin {ℕ}_{0}$
40 39 ex ${⊢}{B}\in {W}\to \left(¬{B}\in \mathrm{Fin}\to \left|{B}\right|\notin {ℕ}_{0}\right)$
41 40 adantl ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(¬{B}\in \mathrm{Fin}\to \left|{B}\right|\notin {ℕ}_{0}\right)$
42 41 impcom ${⊢}\left(¬{B}\in \mathrm{Fin}\wedge \left({A}\in {V}\wedge {B}\in {W}\right)\right)\to \left|{B}\right|\notin {ℕ}_{0}$
43 hashinfxadd ${⊢}\left({B}\in {W}\wedge {A}\in {V}\wedge \left|{B}\right|\notin {ℕ}_{0}\right)\to \left|{B}\right|{+}_{𝑒}\left|{A}\right|=\mathrm{+\infty }$
44 37 38 42 43 syl3anc ${⊢}\left(¬{B}\in \mathrm{Fin}\wedge \left({A}\in {V}\wedge {B}\in {W}\right)\right)\to \left|{B}\right|{+}_{𝑒}\left|{A}\right|=\mathrm{+\infty }$
45 36 44 eqtrd ${⊢}\left(¬{B}\in \mathrm{Fin}\wedge \left({A}\in {V}\wedge {B}\in {W}\right)\right)\to \left|{A}\right|{+}_{𝑒}\left|{B}\right|=\mathrm{+\infty }$
46 45 eqcomd ${⊢}\left(¬{B}\in \mathrm{Fin}\wedge \left({A}\in {V}\wedge {B}\in {W}\right)\right)\to \mathrm{+\infty }=\left|{A}\right|{+}_{𝑒}\left|{B}\right|$
47 46 ex ${⊢}¬{B}\in \mathrm{Fin}\to \left(\left({A}\in {V}\wedge {B}\in {W}\right)\to \mathrm{+\infty }=\left|{A}\right|{+}_{𝑒}\left|{B}\right|\right)$
48 30 47 jaoi ${⊢}\left(¬{A}\in \mathrm{Fin}\vee ¬{B}\in \mathrm{Fin}\right)\to \left(\left({A}\in {V}\wedge {B}\in {W}\right)\to \mathrm{+\infty }=\left|{A}\right|{+}_{𝑒}\left|{B}\right|\right)$
49 20 48 sylbi ${⊢}¬\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left(\left({A}\in {V}\wedge {B}\in {W}\right)\to \mathrm{+\infty }=\left|{A}\right|{+}_{𝑒}\left|{B}\right|\right)$
50 49 imp ${⊢}\left(¬\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\wedge \left({A}\in {V}\wedge {B}\in {W}\right)\right)\to \mathrm{+\infty }=\left|{A}\right|{+}_{𝑒}\left|{B}\right|$
51 19 50 eqtrd ${⊢}\left(¬\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\wedge \left({A}\in {V}\wedge {B}\in {W}\right)\right)\to \left|{A}\cup {B}\right|=\left|{A}\right|{+}_{𝑒}\left|{B}\right|$
52 51 expcom ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(¬\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left|{A}\cup {B}\right|=\left|{A}\right|{+}_{𝑒}\left|{B}\right|\right)$
53 52 3adant3 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\cap {B}=\varnothing \right)\to \left(¬\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left|{A}\cup {B}\right|=\left|{A}\right|{+}_{𝑒}\left|{B}\right|\right)$
54 14 53 pm2.61d ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\cap {B}=\varnothing \right)\to \left|{A}\cup {B}\right|=\left|{A}\right|{+}_{𝑒}\left|{B}\right|$