Theorem hashinfxadd

Description: The extended real addition of the size of an infinite set with the size of an arbitrary set yields plus infinity. (Contributed by Alexander van der Vekens, 20-Dec-2017)

	Ref	Expression
Assertion	hashinfxadd	$$⊢\left(A\in V\wedge B\in W\wedge \left|A\right|\notin {\mathbb{N}}_0\right)\to \left|A\right|{+}_{𝑒}\left|B\right|=\mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		hashnn0pnf	$$⊢A\in V\to \left(\left|A\right|\in {\mathbb{N}}_0\vee \left|A\right|=\mathrm{+\infty }\right)$$
2		df-nel	$$⊢\left|A\right|\notin {\mathbb{N}}_0\leftrightarrow \neg \left|A\right|\in {\mathbb{N}}_0$$
3	2	anbi2i	$$⊢\left(\left(\left|A\right|=\mathrm{+\infty }\vee \left|A\right|\in {\mathbb{N}}_0\right)\wedge \left|A\right|\notin {\mathbb{N}}_0\right)\leftrightarrow \left(\left(\left|A\right|=\mathrm{+\infty }\vee \left|A\right|\in {\mathbb{N}}_0\right)\wedge \neg \left|A\right|\in {\mathbb{N}}_0\right)$$
4		pm5.61	$$⊢\left(\left(\left|A\right|=\mathrm{+\infty }\vee \left|A\right|\in {\mathbb{N}}_0\right)\wedge \neg \left|A\right|\in {\mathbb{N}}_0\right)\leftrightarrow \left(\left|A\right|=\mathrm{+\infty }\wedge \neg \left|A\right|\in {\mathbb{N}}_0\right)$$
5	3 4	sylbb	$$⊢\left(\left(\left|A\right|=\mathrm{+\infty }\vee \left|A\right|\in {\mathbb{N}}_0\right)\wedge \left|A\right|\notin {\mathbb{N}}_0\right)\to \left(\left|A\right|=\mathrm{+\infty }\wedge \neg \left|A\right|\in {\mathbb{N}}_0\right)$$
6	5	ex	$$⊢\left(\left|A\right|=\mathrm{+\infty }\vee \left|A\right|\in {\mathbb{N}}_0\right)\to \left(\left|A\right|\notin {\mathbb{N}}_0\to \left(\left|A\right|=\mathrm{+\infty }\wedge \neg \left|A\right|\in {\mathbb{N}}_0\right)\right)$$
7	6	orcoms	$$⊢\left(\left|A\right|\in {\mathbb{N}}_0\vee \left|A\right|=\mathrm{+\infty }\right)\to \left(\left|A\right|\notin {\mathbb{N}}_0\to \left(\left|A\right|=\mathrm{+\infty }\wedge \neg \left|A\right|\in {\mathbb{N}}_0\right)\right)$$
8	1 7	syl	$$⊢A\in V\to \left(\left|A\right|\notin {\mathbb{N}}_0\to \left(\left|A\right|=\mathrm{+\infty }\wedge \neg \left|A\right|\in {\mathbb{N}}_0\right)\right)$$
9	8	imp	$$⊢\left(A\in V\wedge \left|A\right|\notin {\mathbb{N}}_0\right)\to \left(\left|A\right|=\mathrm{+\infty }\wedge \neg \left|A\right|\in {\mathbb{N}}_0\right)$$
10	9	3adant2	$$⊢\left(A\in V\wedge B\in W\wedge \left|A\right|\notin {\mathbb{N}}_0\right)\to \left(\left|A\right|=\mathrm{+\infty }\wedge \neg \left|A\right|\in {\mathbb{N}}_0\right)$$
11		oveq1	$$⊢\left|A\right|=\mathrm{+\infty }\to \left|A\right|{+}_{𝑒}\left|B\right|=\mathrm{+\infty }{+}_{𝑒}\left|B\right|$$
12		hashxrcl	$$⊢B\in W\to \left|B\right|\in {ℝ}^{*}$$
13		hashnemnf	$$⊢B\in W\to \left|B\right|\ne \mathrm{-\infty }$$
14	12 13	jca	$$⊢B\in W\to \left(\left|B\right|\in {ℝ}^{*}\wedge \left|B\right|\ne \mathrm{-\infty }\right)$$
15	14	3ad2ant2	$$⊢\left(A\in V\wedge B\in W\wedge \left|A\right|\notin {\mathbb{N}}_0\right)\to \left(\left|B\right|\in {ℝ}^{*}\wedge \left|B\right|\ne \mathrm{-\infty }\right)$$
16		xaddpnf2	$$⊢\left(\left|B\right|\in {ℝ}^{*}\wedge \left|B\right|\ne \mathrm{-\infty }\right)\to \mathrm{+\infty }{+}_{𝑒}\left|B\right|=\mathrm{+\infty }$$
17	15 16	syl	$$⊢\left(A\in V\wedge B\in W\wedge \left|A\right|\notin {\mathbb{N}}_0\right)\to \mathrm{+\infty }{+}_{𝑒}\left|B\right|=\mathrm{+\infty }$$
18	11 17	sylan9eqr	$$⊢\left(\left(A\in V\wedge B\in W\wedge \left|A\right|\notin {\mathbb{N}}_0\right)\wedge \left|A\right|=\mathrm{+\infty }\right)\to \left|A\right|{+}_{𝑒}\left|B\right|=\mathrm{+\infty }$$
19	18	expcom	$$⊢\left|A\right|=\mathrm{+\infty }\to \left(\left(A\in V\wedge B\in W\wedge \left|A\right|\notin {\mathbb{N}}_0\right)\to \left|A\right|{+}_{𝑒}\left|B\right|=\mathrm{+\infty }\right)$$
20	19	adantr	$$⊢\left(\left|A\right|=\mathrm{+\infty }\wedge \neg \left|A\right|\in {\mathbb{N}}_0\right)\to \left(\left(A\in V\wedge B\in W\wedge \left|A\right|\notin {\mathbb{N}}_0\right)\to \left|A\right|{+}_{𝑒}\left|B\right|=\mathrm{+\infty }\right)$$
21	10 20	mpcom	$$⊢\left(A\in V\wedge B\in W\wedge \left|A\right|\notin {\mathbb{N}}_0\right)\to \left|A\right|{+}_{𝑒}\left|B\right|=\mathrm{+\infty }$$