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 ⊢Ⅎ_kD
esumc.1 ⊢Ⅎkφ
esumc.2 ⊢Ⅎ_kA
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∈AB=∑*y∈z|∃k∈Az=CD

Proof

Step Hyp Ref Expression
1 esumc.0 ⊢Ⅎ_kD
2 esumc.1 ⊢Ⅎkφ
3 esumc.2 ⊢Ⅎ_kA
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 ⊢Ⅎ_yB
10 nfre1 ⊢Ⅎk∃k∈Az=C
11 10 nfab ⊢Ⅎ_kz|∃k∈Az=C
12 nfmpt1 ⊢Ⅎ_kk∈A⟼C
13 elex ⊢A∈V→A∈V
14 5 13 syl ⊢φ→A∈V
15 3 14 abrexexd ⊢φ→z|∃k∈Az=C∈V
16 8 ex ⊢φ→k∈A→C∈W
17 2 16 ralrimi ⊢φ→∀k∈AC∈W
18 3 fnmptf ⊢∀k∈AC∈W→k∈A⟼CFnA
19 17 18 syl ⊢φ→k∈A⟼CFnA
20 eqid ⊢k∈A⟼C=k∈A⟼C
21 20 rnmpt ⊢ran⁡k∈A⟼C=z|∃k∈Az=C
22 21 a1i ⊢φ→ran⁡k∈A⟼C=z|∃k∈Az=C
23 dff1o2 ⊢k∈A⟼C:A⟶1-1 ontoz|∃k∈Az=C↔k∈A⟼CFnA∧Fun⁡k∈A⟼C-1∧ran⁡k∈A⟼C=z|∃k∈Az=C
24 19 6 22 23 syl3anbrc ⊢φ→k∈A⟼C:A⟶1-1 ontoz|∃k∈Az=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∈Az=C↔∃k∈Ay=C
31 28 30 elab ⊢y∈z|∃k∈Az=C↔∃k∈Ay=C
32 4 reximi ⊢∃k∈Ay=C→∃k∈AD=B
33 31 32 sylbi ⊢y∈z|∃k∈Az=C→∃k∈AD=B
34 nfcv ⊢Ⅎ_k0+∞
35 1 34 nfel ⊢ℲkD∈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∈AD=B→D∈0+∞
40 39 imp ⊢φ∧∃k∈AD=B→D∈0+∞
41 33 40 sylan2 ⊢φ∧y∈z|∃k∈Az=C→D∈0+∞
42 2 1 9 11 3 12 4 15 24 27 41 esumf1o ⊢φ→∑*y∈z|∃k∈Az=CD=∑*k∈AB
43 42 eqcomd ⊢φ→∑*k∈AB=∑*y∈z|∃k∈Az=CD