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 \in V \land B \in W \land A \cap B = \emptyset) \to \|A \cup B\| = \|A\| +_{𝑒} \|B\|$

Proof

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

Metamath Proof Explorer

Theorem hashunx

Proof