Metamath Proof Explorer

Theorem esumc

Description: Convert from the collection form to the class-variable form of a sum. (Contributed by Thierry Arnoux, 10-May-2017)

Ref Expression
Hypotheses esumc.0 ⊢ Ⅎ _ k D
esumc.1 ⊢ Ⅎ k φ
esumc.2 ⊢ Ⅎ _ k A
esumc.3 ⊢ y = C → D = B
esumc.4 ⊢ φ → A ∈ V
esumc.5 ⊢ φ → Fun ⁡ k ∈ A ⟼ C -1
esumc.6 ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
esumc.7 ⊢ φ ∧ k ∈ A → C ∈ W
Assertion esumc ⊢ φ → ∑ * k ∈ A B = ∑ * y ∈ z | ∃ k ∈ A z = C D

Proof

Step Hyp Ref Expression
1 esumc.0 ⊢ Ⅎ _ k D
2 esumc.1 ⊢ Ⅎ k φ
3 esumc.2 ⊢ Ⅎ _ k A
4 esumc.3 ⊢ y = C → D = B
5 esumc.4 ⊢ φ → A ∈ V
6 esumc.5 ⊢ φ → Fun ⁡ k ∈ A ⟼ C -1
7 esumc.6 ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
8 esumc.7 ⊢ φ ∧ k ∈ A → C ∈ W
9 nfcv ⊢ Ⅎ _ y B
10 nfre1 ⊢ Ⅎ k ∃ k ∈ A z = C
11 10 nfab ⊢ Ⅎ _ k z | ∃ k ∈ A z = C
12 nfmpt1 ⊢ Ⅎ _ k k ∈ A ⟼ C
13 elex ⊢ A ∈ V → A ∈ V
14 5 13 syl ⊢ φ → A ∈ V
15 3 14 abrexexd ⊢ φ → z | ∃ k ∈ A z = C ∈ V
16 8 ex ⊢ φ → k ∈ A → C ∈ W
17 2 16 ralrimi ⊢ φ → ∀ k ∈ A C ∈ W
18 3 fnmptf ⊢ ∀ k ∈ A C ∈ W → k ∈ A ⟼ C Fn A
19 17 18 syl ⊢ φ → k ∈ A ⟼ C Fn A
20 eqid ⊢ k ∈ A ⟼ C = k ∈ A ⟼ C
21 20 rnmpt ⊢ ran ⁡ k ∈ A ⟼ C = z | ∃ k ∈ A z = C
22 21 a1i ⊢ φ → ran ⁡ k ∈ A ⟼ C = z | ∃ k ∈ A z = C
23 dff1o2 ⊢ k ∈ A ⟼ C : A ⟶ 1-1 onto z | ∃ k ∈ A z = C ↔ k ∈ A ⟼ C Fn A ∧ Fun ⁡ k ∈ A ⟼ C -1 ∧ ran ⁡ k ∈ A ⟼ C = z | ∃ k ∈ A z = C
24 19 6 22 23 syl3anbrc ⊢ φ → k ∈ A ⟼ C : A ⟶ 1-1 onto z | ∃ k ∈ A z = C
25 simpr ⊢ φ ∧ k ∈ A → k ∈ A
26 3 fvmpt2f ⊢ k ∈ A ∧ C ∈ W → k ∈ A ⟼ C ⁡ k = C
27 25 8 26 syl2anc ⊢ φ ∧ k ∈ A → k ∈ A ⟼ C ⁡ k = C
28 vex ⊢ y ∈ V
29 eqeq1 ⊢ z = y → z = C ↔ y = C
30 29 rexbidv ⊢ z = y → ∃ k ∈ A z = C ↔ ∃ k ∈ A y = C
31 28 30 elab ⊢ y ∈ z | ∃ k ∈ A z = C ↔ ∃ k ∈ A y = C
32 4 reximi ⊢ ∃ k ∈ A y = C → ∃ k ∈ A D = B
33 31 32 sylbi ⊢ y ∈ z | ∃ k ∈ A z = C → ∃ k ∈ A D = B
34 nfcv ⊢ Ⅎ _ k 0 +∞
35 1 34 nfel ⊢ Ⅎ k D ∈ 0 +∞
36 eleq1 ⊢ D = B → D ∈ 0 +∞ ↔ B ∈ 0 +∞
37 7 36 syl5ibrcom ⊢ φ ∧ k ∈ A → D = B → D ∈ 0 +∞
38 37 ex ⊢ φ → k ∈ A → D = B → D ∈ 0 +∞
39 2 35 38 rexlimd ⊢ φ → ∃ k ∈ A D = B → D ∈ 0 +∞
40 39 imp ⊢ φ ∧ ∃ k ∈ A D = B → D ∈ 0 +∞
41 33 40 sylan2 ⊢ φ ∧ y ∈ z | ∃ k ∈ A z = C → D ∈ 0 +∞
42 2 1 9 11 3 12 4 15 24 27 41 esumf1o ⊢ φ → ∑ * y ∈ z | ∃ k ∈ A z = C D = ∑ * k ∈ A B
43 42 eqcomd ⊢ φ → ∑ * k ∈ A B = ∑ * y ∈ z | ∃ k ∈ A z = C D