Step | Hyp | Ref
| Expression |
1 | | nn0addcl 11205 |
. . . . . . 7
⊢
(((#‘{𝑥 ∈
𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℕ0 ∧
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℕ0) →
((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) + (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) ∈
ℕ0) |
2 | | elun1 3742 |
. . . . . . 7
⊢
(((#‘{𝑥 ∈
𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) + (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) ∈ ℕ0 →
((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) + (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) ∈ (ℕ0 ∪
{+∞})) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢
(((#‘{𝑥 ∈
𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℕ0 ∧
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℕ0) →
((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) + (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) ∈ (ℕ0 ∪
{+∞})) |
4 | | nn0re 11178 |
. . . . . . 7
⊢
((#‘{𝑥 ∈
𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℕ0 →
(#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℝ) |
5 | | nn0re 11178 |
. . . . . . 7
⊢
((#‘{𝑥 ∈
𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℕ0 →
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℝ) |
6 | | rexadd 11937 |
. . . . . . . 8
⊢
(((#‘{𝑥 ∈
𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℝ ∧ (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℝ) → ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) = ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) + (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}))) |
7 | 6 | eleq1d 2672 |
. . . . . . 7
⊢
(((#‘{𝑥 ∈
𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℝ ∧ (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℝ) → (((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) ∈ (ℕ0 ∪
{+∞}) ↔ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) + (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) ∈ (ℕ0 ∪
{+∞}))) |
8 | 4, 5, 7 | syl2an 493 |
. . . . . 6
⊢
(((#‘{𝑥 ∈
𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℕ0 ∧
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℕ0) →
(((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) ∈ (ℕ0 ∪
{+∞}) ↔ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) + (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) ∈ (ℕ0 ∪
{+∞}))) |
9 | 3, 8 | mpbird 246 |
. . . . 5
⊢
(((#‘{𝑥 ∈
𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℕ0 ∧
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℕ0) →
((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) ∈ (ℕ0 ∪
{+∞})) |
10 | 9 | a1d 25 |
. . . 4
⊢
(((#‘{𝑥 ∈
𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℕ0 ∧
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℕ0) →
(((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉) → ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) ∈ (ℕ0 ∪
{+∞}))) |
11 | | ianor 508 |
. . . . 5
⊢ (¬
((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℕ0 ∧
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℕ0) ↔ (¬
(#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℕ0 ∨ ¬
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈
ℕ0)) |
12 | | df-nel 2783 |
. . . . . . . . . 10
⊢
((#‘{𝑥 ∈
𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∉ ℕ0 ↔ ¬
(#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈
ℕ0) |
13 | | rabexg 4739 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑋 → {𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)} ∈ V) |
14 | 13 | 3ad2ant3 1077 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) → {𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)} ∈ V) |
15 | 14 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢
(((#‘{𝑥 ∈
𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∉ ℕ0 ∧ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉)) → {𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)} ∈ V) |
16 | | rabexg 4739 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑋 → {𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}} ∈ V) |
17 | 16 | 3ad2ant3 1077 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) → {𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}} ∈ V) |
18 | 17 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢
(((#‘{𝑥 ∈
𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∉ ℕ0 ∧ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉)) → {𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}} ∈ V) |
19 | | simpl 472 |
. . . . . . . . . . . 12
⊢
(((#‘{𝑥 ∈
𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∉ ℕ0 ∧ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉)) → (#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∉
ℕ0) |
20 | | hashinfxadd 13035 |
. . . . . . . . . . . 12
⊢ (({𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)} ∈ V ∧ {𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}} ∈ V ∧ (#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∉ ℕ0) →
((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) = +∞) |
21 | 15, 18, 19, 20 | syl3anc 1318 |
. . . . . . . . . . 11
⊢
(((#‘{𝑥 ∈
𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∉ ℕ0 ∧ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉)) → ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) = +∞) |
22 | 21 | ex 449 |
. . . . . . . . . 10
⊢
((#‘{𝑥 ∈
𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∉ ℕ0 →
(((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉) → ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) = +∞)) |
23 | 12, 22 | sylbir 224 |
. . . . . . . . 9
⊢ (¬
(#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℕ0 →
(((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉) → ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) = +∞)) |
24 | | df-nel 2783 |
. . . . . . . . . 10
⊢
((#‘{𝑥 ∈
𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∉ ℕ0 ↔ ¬
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈
ℕ0) |
25 | 17 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢
(((#‘{𝑥 ∈
𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∉ ℕ0 ∧ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉)) → {𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}} ∈ V) |
26 | 14 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢
(((#‘{𝑥 ∈
𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∉ ℕ0 ∧ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉)) → {𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)} ∈ V) |
27 | | simpl 472 |
. . . . . . . . . . . 12
⊢
(((#‘{𝑥 ∈
𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∉ ℕ0 ∧ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉)) → (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∉
ℕ0) |
28 | | hashxrcl 13010 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}} ∈ V → (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈
ℝ*) |
29 | | hashxrcl 13010 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)} ∈ V → (#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈
ℝ*) |
30 | 28, 29 | anim12ci 589 |
. . . . . . . . . . . . . . 15
⊢ (({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}} ∈ V ∧ {𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)} ∈ V) → ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℝ* ∧
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈
ℝ*)) |
31 | 30 | 3adant3 1074 |
. . . . . . . . . . . . . 14
⊢ (({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}} ∈ V ∧ {𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)} ∈ V ∧ (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∉ ℕ0) →
((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℝ* ∧
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈
ℝ*)) |
32 | | xaddcom 11945 |
. . . . . . . . . . . . . 14
⊢
(((#‘{𝑥 ∈
𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℝ* ∧
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℝ*) →
((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) = ((#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}))) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . 13
⊢ (({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}} ∈ V ∧ {𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)} ∈ V ∧ (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∉ ℕ0) →
((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) = ((#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}))) |
34 | | hashinfxadd 13035 |
. . . . . . . . . . . . 13
⊢ (({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}} ∈ V ∧ {𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)} ∈ V ∧ (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∉ ℕ0) →
((#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)})) = +∞) |
35 | 33, 34 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}} ∈ V ∧ {𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)} ∈ V ∧ (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∉ ℕ0) →
((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) = +∞) |
36 | 25, 26, 27, 35 | syl3anc 1318 |
. . . . . . . . . . 11
⊢
(((#‘{𝑥 ∈
𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∉ ℕ0 ∧ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉)) → ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) = +∞) |
37 | 36 | ex 449 |
. . . . . . . . . 10
⊢
((#‘{𝑥 ∈
𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∉ ℕ0 →
(((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉) → ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) = +∞)) |
38 | 24, 37 | sylbir 224 |
. . . . . . . . 9
⊢ (¬
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℕ0 →
(((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉) → ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) = +∞)) |
39 | 23, 38 | jaoi 393 |
. . . . . . . 8
⊢ ((¬
(#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℕ0 ∨ ¬
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℕ0) →
(((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉) → ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) = +∞)) |
40 | 39 | imp 444 |
. . . . . . 7
⊢ (((¬
(#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℕ0 ∨ ¬
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℕ0) ∧ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉)) → ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) = +∞) |
41 | | pnfex 9972 |
. . . . . . . . . 10
⊢ +∞
∈ V |
42 | 41 | snid 4155 |
. . . . . . . . 9
⊢ +∞
∈ {+∞} |
43 | 42 | olci 405 |
. . . . . . . 8
⊢ (+∞
∈ ℕ0 ∨ +∞ ∈ {+∞}) |
44 | | elun 3715 |
. . . . . . . 8
⊢ (+∞
∈ (ℕ0 ∪ {+∞}) ↔ (+∞ ∈
ℕ0 ∨ +∞ ∈ {+∞})) |
45 | 43, 44 | mpbir 220 |
. . . . . . 7
⊢ +∞
∈ (ℕ0 ∪ {+∞}) |
46 | 40, 45 | syl6eqel 2696 |
. . . . . 6
⊢ (((¬
(#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℕ0 ∨ ¬
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℕ0) ∧ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉)) → ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) ∈ (ℕ0 ∪
{+∞})) |
47 | 46 | ex 449 |
. . . . 5
⊢ ((¬
(#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℕ0 ∨ ¬
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℕ0) →
(((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉) → ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) ∈ (ℕ0 ∪
{+∞}))) |
48 | 11, 47 | sylbi 206 |
. . . 4
⊢ (¬
((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) ∈ ℕ0 ∧
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) ∈ ℕ0) →
(((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉) → ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) ∈ (ℕ0 ∪
{+∞}))) |
49 | 10, 48 | pm2.61i 175 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑢 ∈ 𝑉) → ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) ∈ (ℕ0 ∪
{+∞})) |
50 | | eqid 2610 |
. . 3
⊢ (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}))) = (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}))) |
51 | 49, 50 | fmptd 6292 |
. 2
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) → (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}))):𝑉⟶(ℕ0 ∪
{+∞})) |
52 | | vdgrfval 26422 |
. . 3
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) → (𝑉 VDeg 𝐸) = (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})))) |
53 | 52 | feq1d 5943 |
. 2
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) → ((𝑉 VDeg 𝐸):𝑉⟶(ℕ0 ∪
{+∞}) ↔ (𝑢
∈ 𝑉 ↦
((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}))):𝑉⟶(ℕ0 ∪
{+∞}))) |
54 | 51, 53 | mpbird 246 |
1
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) → (𝑉 VDeg 𝐸):𝑉⟶(ℕ0 ∪
{+∞})) |