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 ⊢ A ∈ V ∧ B ∈ W ∧ A ∩ B = ∅ → A ∪ B = A + 𝑒 B

Proof

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