Metamath Proof Explorer

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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( ♯ ‘ 𝐴 ) ∉ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) = +∞ )

Proof

Step Hyp Ref Expression
1 hashnn0pnf ⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝐴 ) = +∞ ) )
2 df-nel ⊢ ( ( ♯ ‘ 𝐴 ) ∉ ℕ0 ↔ ¬ ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
3 2 anbi2i ⊢ ( ( ( ( ♯ ‘ 𝐴 ) = +∞ ∨ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝐴 ) ∉ ℕ0 ) ↔ ( ( ( ♯ ‘ 𝐴 ) = +∞ ∨ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ ¬ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) )
4 pm5.61 ⊢ ( ( ( ( ♯ ‘ 𝐴 ) = +∞ ∨ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ ¬ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ↔ ( ( ♯ ‘ 𝐴 ) = +∞ ∧ ¬ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) )
5 3 4 sylbb ⊢ ( ( ( ( ♯ ‘ 𝐴 ) = +∞ ∨ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ ( ♯ ‘ 𝐴 ) ∉ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) = +∞ ∧ ¬ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) )
6 5 ex ⊢ ( ( ( ♯ ‘ 𝐴 ) = +∞ ∨ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) ∉ ℕ0 → ( ( ♯ ‘ 𝐴 ) = +∞ ∧ ¬ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ) )
7 6 orcoms ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝐴 ) = +∞ ) → ( ( ♯ ‘ 𝐴 ) ∉ ℕ0 → ( ( ♯ ‘ 𝐴 ) = +∞ ∧ ¬ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ) )
8 1 7 syl ⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) ∉ ℕ0 → ( ( ♯ ‘ 𝐴 ) = +∞ ∧ ¬ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ) )
9 8 imp ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ♯ ‘ 𝐴 ) ∉ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) = +∞ ∧ ¬ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) )
10 9 3adant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( ♯ ‘ 𝐴 ) ∉ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) = +∞ ∧ ¬ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) )
11 oveq1 ⊢ ( ( ♯ ‘ 𝐴 ) = +∞ → ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) = ( +∞ +𝑒 ( ♯ ‘ 𝐵 ) ) )
12 hashxrcl ⊢ ( 𝐵 ∈ 𝑊 → ( ♯ ‘ 𝐵 ) ∈ ℝ* )
13 hashnemnf ⊢ ( 𝐵 ∈ 𝑊 → ( ♯ ‘ 𝐵 ) ≠ -∞ )
14 12 13 jca ⊢ ( 𝐵 ∈ 𝑊 → ( ( ♯ ‘ 𝐵 ) ∈ ℝ* ∧ ( ♯ ‘ 𝐵 ) ≠ -∞ ) )
15 14 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( ♯ ‘ 𝐴 ) ∉ ℕ0 ) → ( ( ♯ ‘ 𝐵 ) ∈ ℝ* ∧ ( ♯ ‘ 𝐵 ) ≠ -∞ ) )
16 xaddpnf2 ⊢ ( ( ( ♯ ‘ 𝐵 ) ∈ ℝ* ∧ ( ♯ ‘ 𝐵 ) ≠ -∞ ) → ( +∞ +𝑒 ( ♯ ‘ 𝐵 ) ) = +∞ )
17 15 16 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( ♯ ‘ 𝐴 ) ∉ ℕ0 ) → ( +∞ +𝑒 ( ♯ ‘ 𝐵 ) ) = +∞ )
18 11 17 sylan9eqr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( ♯ ‘ 𝐴 ) ∉ ℕ0 ) ∧ ( ♯ ‘ 𝐴 ) = +∞ ) → ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) = +∞ )
19 18 expcom ⊢ ( ( ♯ ‘ 𝐴 ) = +∞ → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( ♯ ‘ 𝐴 ) ∉ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) = +∞ ) )
20 19 adantr ⊢ ( ( ( ♯ ‘ 𝐴 ) = +∞ ∧ ¬ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( ♯ ‘ 𝐴 ) ∉ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) = +∞ ) )
21 10 20 mpcom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ( ♯ ‘ 𝐴 ) ∉ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ 𝐵 ) ) = +∞ )