# Metamath Proof Explorer

## Theorem reprsuc

Description: Express the representations recursively. (Contributed by Thierry Arnoux, 5-Dec-2021)

Ref Expression
Hypotheses reprval.a ${⊢}{\phi }\to {A}\subseteq ℕ$
reprval.m ${⊢}{\phi }\to {M}\in ℤ$
reprval.s ${⊢}{\phi }\to {S}\in {ℕ}_{0}$
reprsuc.f ${⊢}{F}=\left({c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)⟼{c}\cup \left\{⟨{S},{b}⟩\right\}\right)$
Assertion reprsuc ${⊢}{\phi }\to {A}\mathrm{repr}\left({S}+1\right){M}=\bigcup _{{b}\in {A}}\mathrm{ran}{F}$

### Proof

Step Hyp Ref Expression
1 reprval.a ${⊢}{\phi }\to {A}\subseteq ℕ$
2 reprval.m ${⊢}{\phi }\to {M}\in ℤ$
3 reprval.s ${⊢}{\phi }\to {S}\in {ℕ}_{0}$
4 reprsuc.f ${⊢}{F}=\left({c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)⟼{c}\cup \left\{⟨{S},{b}⟩\right\}\right)$
5 1nn0 ${⊢}1\in {ℕ}_{0}$
6 5 a1i ${⊢}{\phi }\to 1\in {ℕ}_{0}$
7 3 6 nn0addcld ${⊢}{\phi }\to {S}+1\in {ℕ}_{0}$
8 1 2 7 reprval ${⊢}{\phi }\to {A}\mathrm{repr}\left({S}+1\right){M}=\left\{{c}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)|\sum _{{a}\in \left(0..^{S}+1\right)}{c}\left({a}\right)={M}\right\}$
9 simplr ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)$
10 elmapi ${⊢}{e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\to {e}:\left(0..^{S}+1\right)⟶{A}$
11 9 10 syl ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {e}:\left(0..^{S}+1\right)⟶{A}$
12 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {S}\in {ℕ}_{0}$
13 fzonn0p1 ${⊢}{S}\in {ℕ}_{0}\to {S}\in \left(0..^{S}+1\right)$
14 12 13 syl ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {S}\in \left(0..^{S}+1\right)$
15 11 14 ffvelrnd ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {e}\left({S}\right)\in {A}$
16 simpr ${⊢}\left(\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\wedge {b}={e}\left({S}\right)\right)\to {b}={e}\left({S}\right)$
17 16 oveq2d ${⊢}\left(\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\wedge {b}={e}\left({S}\right)\right)\to {M}-{b}={M}-{e}\left({S}\right)$
18 17 oveq2d ${⊢}\left(\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\wedge {b}={e}\left({S}\right)\right)\to {A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)={A}\mathrm{repr}\left({S}\right)\left({M}-{e}\left({S}\right)\right)$
19 opeq2 ${⊢}{b}={e}\left({S}\right)\to ⟨{S},{b}⟩=⟨{S},{e}\left({S}\right)⟩$
20 19 sneqd ${⊢}{b}={e}\left({S}\right)\to \left\{⟨{S},{b}⟩\right\}=\left\{⟨{S},{e}\left({S}\right)⟩\right\}$
21 20 uneq2d ${⊢}{b}={e}\left({S}\right)\to {c}\cup \left\{⟨{S},{b}⟩\right\}={c}\cup \left\{⟨{S},{e}\left({S}\right)⟩\right\}$
22 21 eqeq2d ${⊢}{b}={e}\left({S}\right)\to \left({e}={c}\cup \left\{⟨{S},{b}⟩\right\}↔{e}={c}\cup \left\{⟨{S},{e}\left({S}\right)⟩\right\}\right)$
23 22 adantl ${⊢}\left(\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\wedge {b}={e}\left({S}\right)\right)\to \left({e}={c}\cup \left\{⟨{S},{b}⟩\right\}↔{e}={c}\cup \left\{⟨{S},{e}\left({S}\right)⟩\right\}\right)$
24 18 23 rexeqbidv ${⊢}\left(\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\wedge {b}={e}\left({S}\right)\right)\to \left(\exists {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\phantom{\rule{.4em}{0ex}}{e}={c}\cup \left\{⟨{S},{b}⟩\right\}↔\exists {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{e}\left({S}\right)\right)\right)\phantom{\rule{.4em}{0ex}}{e}={c}\cup \left\{⟨{S},{e}\left({S}\right)⟩\right\}\right)$
25 10 adantl ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to {e}:\left(0..^{S}+1\right)⟶{A}$
26 3 adantr ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to {S}\in {ℕ}_{0}$
27 fzossfzop1 ${⊢}{S}\in {ℕ}_{0}\to \left(0..^{S}\right)\subseteq \left(0..^{S}+1\right)$
28 26 27 syl ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to \left(0..^{S}\right)\subseteq \left(0..^{S}+1\right)$
29 25 28 fssresd ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to \left({{e}↾}_{\left(0..^{S}\right)}\right):\left(0..^{S}\right)⟶{A}$
30 29 adantr ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to \left({{e}↾}_{\left(0..^{S}\right)}\right):\left(0..^{S}\right)⟶{A}$
31 nnex ${⊢}ℕ\in \mathrm{V}$
32 31 a1i ${⊢}{\phi }\to ℕ\in \mathrm{V}$
33 32 1 ssexd ${⊢}{\phi }\to {A}\in \mathrm{V}$
34 fzofi ${⊢}\left(0..^{S}\right)\in \mathrm{Fin}$
35 34 elexi ${⊢}\left(0..^{S}\right)\in \mathrm{V}$
36 elmapg ${⊢}\left({A}\in \mathrm{V}\wedge \left(0..^{S}\right)\in \mathrm{V}\right)\to \left({{e}↾}_{\left(0..^{S}\right)}\in \left({{A}}^{\left(0..^{S}\right)}\right)↔\left({{e}↾}_{\left(0..^{S}\right)}\right):\left(0..^{S}\right)⟶{A}\right)$
37 33 35 36 sylancl ${⊢}{\phi }\to \left({{e}↾}_{\left(0..^{S}\right)}\in \left({{A}}^{\left(0..^{S}\right)}\right)↔\left({{e}↾}_{\left(0..^{S}\right)}\right):\left(0..^{S}\right)⟶{A}\right)$
38 37 ad2antrr ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to \left({{e}↾}_{\left(0..^{S}\right)}\in \left({{A}}^{\left(0..^{S}\right)}\right)↔\left({{e}↾}_{\left(0..^{S}\right)}\right):\left(0..^{S}\right)⟶{A}\right)$
39 30 38 mpbird ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {{e}↾}_{\left(0..^{S}\right)}\in \left({{A}}^{\left(0..^{S}\right)}\right)$
40 34 a1i ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to \left(0..^{S}\right)\in \mathrm{Fin}$
41 nnsscn ${⊢}ℕ\subseteq ℂ$
42 41 a1i ${⊢}{\phi }\to ℕ\subseteq ℂ$
43 1 42 sstrd ${⊢}{\phi }\to {A}\subseteq ℂ$
44 43 ad2antrr ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {A}\subseteq ℂ$
45 29 ffvelrnda ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge {a}\in \left(0..^{S}\right)\right)\to \left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)\in {A}$
46 44 45 sseldd ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge {a}\in \left(0..^{S}\right)\right)\to \left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)\in ℂ$
47 40 46 fsumcl ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to \sum _{{a}\in \left(0..^{S}\right)}\left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)\in ℂ$
48 47 adantr ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to \sum _{{a}\in \left(0..^{S}\right)}\left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)\in ℂ$
49 43 adantr ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to {A}\subseteq ℂ$
50 26 13 syl ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to {S}\in \left(0..^{S}+1\right)$
51 25 50 ffvelrnd ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to {e}\left({S}\right)\in {A}$
52 49 51 sseldd ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to {e}\left({S}\right)\in ℂ$
53 52 adantr ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {e}\left({S}\right)\in ℂ$
54 48 53 pncand ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to \sum _{{a}\in \left(0..^{S}\right)}\left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)+{e}\left({S}\right)-{e}\left({S}\right)=\sum _{{a}\in \left(0..^{S}\right)}\left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)$
55 nfv ${⊢}Ⅎ{a}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)$
56 nfcv ${⊢}\underset{_}{Ⅎ}{a}\phantom{\rule{.4em}{0ex}}{e}\left({S}\right)$
57 fzonel ${⊢}¬{S}\in \left(0..^{S}\right)$
58 57 a1i ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to ¬{S}\in \left(0..^{S}\right)$
59 25 adantr ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {e}:\left(0..^{S}+1\right)⟶{A}$
60 28 sselda ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {a}\in \left(0..^{S}+1\right)$
61 59 60 ffvelrnd ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {e}\left({a}\right)\in {A}$
62 44 61 sseldd ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {e}\left({a}\right)\in ℂ$
63 fveq2 ${⊢}{a}={S}\to {e}\left({a}\right)={e}\left({S}\right)$
64 55 56 40 26 58 62 63 52 fsumsplitsn ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to \sum _{{a}\in \left(0..^{S}\right)\cup \left\{{S}\right\}}{e}\left({a}\right)=\sum _{{a}\in \left(0..^{S}\right)}{e}\left({a}\right)+{e}\left({S}\right)$
65 fzosplitsn ${⊢}{S}\in {ℤ}_{\ge 0}\to \left(0..^{S}+1\right)=\left(0..^{S}\right)\cup \left\{{S}\right\}$
66 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
67 65 66 eleq2s ${⊢}{S}\in {ℕ}_{0}\to \left(0..^{S}+1\right)=\left(0..^{S}\right)\cup \left\{{S}\right\}$
68 26 67 syl ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to \left(0..^{S}+1\right)=\left(0..^{S}\right)\cup \left\{{S}\right\}$
69 68 sumeq1d ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)=\sum _{{a}\in \left(0..^{S}\right)\cup \left\{{S}\right\}}{e}\left({a}\right)$
70 simpr ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {a}\in \left(0..^{S}\right)$
71 70 fvresd ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge {a}\in \left(0..^{S}\right)\right)\to \left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)={e}\left({a}\right)$
72 71 sumeq2dv ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to \sum _{{a}\in \left(0..^{S}\right)}\left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)=\sum _{{a}\in \left(0..^{S}\right)}{e}\left({a}\right)$
73 72 oveq1d ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to \sum _{{a}\in \left(0..^{S}\right)}\left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)+{e}\left({S}\right)=\sum _{{a}\in \left(0..^{S}\right)}{e}\left({a}\right)+{e}\left({S}\right)$
74 64 69 73 3eqtr4d ${⊢}\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\to \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)=\sum _{{a}\in \left(0..^{S}\right)}\left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)+{e}\left({S}\right)$
75 74 adantr ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)=\sum _{{a}\in \left(0..^{S}\right)}\left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)+{e}\left({S}\right)$
76 simpr ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}$
77 75 76 eqtr3d ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to \sum _{{a}\in \left(0..^{S}\right)}\left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)+{e}\left({S}\right)={M}$
78 77 oveq1d ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to \sum _{{a}\in \left(0..^{S}\right)}\left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)+{e}\left({S}\right)-{e}\left({S}\right)={M}-{e}\left({S}\right)$
79 54 78 eqtr3d ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to \sum _{{a}\in \left(0..^{S}\right)}\left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)={M}-{e}\left({S}\right)$
80 39 79 jca ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to \left({{e}↾}_{\left(0..^{S}\right)}\in \left({{A}}^{\left(0..^{S}\right)}\right)\wedge \sum _{{a}\in \left(0..^{S}\right)}\left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)={M}-{e}\left({S}\right)\right)$
81 fveq1 ${⊢}{d}={{e}↾}_{\left(0..^{S}\right)}\to {d}\left({a}\right)=\left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)$
82 81 sumeq2sdv ${⊢}{d}={{e}↾}_{\left(0..^{S}\right)}\to \sum _{{a}\in \left(0..^{S}\right)}{d}\left({a}\right)=\sum _{{a}\in \left(0..^{S}\right)}\left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)$
83 82 eqeq1d ${⊢}{d}={{e}↾}_{\left(0..^{S}\right)}\to \left(\sum _{{a}\in \left(0..^{S}\right)}{d}\left({a}\right)={M}-{e}\left({S}\right)↔\sum _{{a}\in \left(0..^{S}\right)}\left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)={M}-{e}\left({S}\right)\right)$
84 83 elrab ${⊢}{{e}↾}_{\left(0..^{S}\right)}\in \left\{{d}\in \left({{A}}^{\left(0..^{S}\right)}\right)|\sum _{{a}\in \left(0..^{S}\right)}{d}\left({a}\right)={M}-{e}\left({S}\right)\right\}↔\left({{e}↾}_{\left(0..^{S}\right)}\in \left({{A}}^{\left(0..^{S}\right)}\right)\wedge \sum _{{a}\in \left(0..^{S}\right)}\left({{e}↾}_{\left(0..^{S}\right)}\right)\left({a}\right)={M}-{e}\left({S}\right)\right)$
85 80 84 sylibr ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {{e}↾}_{\left(0..^{S}\right)}\in \left\{{d}\in \left({{A}}^{\left(0..^{S}\right)}\right)|\sum _{{a}\in \left(0..^{S}\right)}{d}\left({a}\right)={M}-{e}\left({S}\right)\right\}$
86 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {A}\subseteq ℕ$
87 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {M}\in ℤ$
88 nnssz ${⊢}ℕ\subseteq ℤ$
89 1 88 sstrdi ${⊢}{\phi }\to {A}\subseteq ℤ$
90 89 ad2antrr ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {A}\subseteq ℤ$
91 90 15 sseldd ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {e}\left({S}\right)\in ℤ$
92 87 91 zsubcld ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {M}-{e}\left({S}\right)\in ℤ$
93 86 92 12 reprval ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {A}\mathrm{repr}\left({S}\right)\left({M}-{e}\left({S}\right)\right)=\left\{{d}\in \left({{A}}^{\left(0..^{S}\right)}\right)|\sum _{{a}\in \left(0..^{S}\right)}{d}\left({a}\right)={M}-{e}\left({S}\right)\right\}$
94 85 93 eleqtrrd ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {{e}↾}_{\left(0..^{S}\right)}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{e}\left({S}\right)\right)\right)$
95 simpr ${⊢}\left(\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\wedge {c}={{e}↾}_{\left(0..^{S}\right)}\right)\to {c}={{e}↾}_{\left(0..^{S}\right)}$
96 95 uneq1d ${⊢}\left(\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\wedge {c}={{e}↾}_{\left(0..^{S}\right)}\right)\to {c}\cup \left\{⟨{S},{e}\left({S}\right)⟩\right\}=\left({{e}↾}_{\left(0..^{S}\right)}\right)\cup \left\{⟨{S},{e}\left({S}\right)⟩\right\}$
97 96 eqeq2d ${⊢}\left(\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\wedge {c}={{e}↾}_{\left(0..^{S}\right)}\right)\to \left({e}={c}\cup \left\{⟨{S},{e}\left({S}\right)⟩\right\}↔{e}=\left({{e}↾}_{\left(0..^{S}\right)}\right)\cup \left\{⟨{S},{e}\left({S}\right)⟩\right\}\right)$
98 11 ffnd ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {e}Fn\left(0..^{S}+1\right)$
99 fnsnsplit ${⊢}\left({e}Fn\left(0..^{S}+1\right)\wedge {S}\in \left(0..^{S}+1\right)\right)\to {e}=\left({{e}↾}_{\left(\left(0..^{S}+1\right)\setminus \left\{{S}\right\}\right)}\right)\cup \left\{⟨{S},{e}\left({S}\right)⟩\right\}$
100 98 14 99 syl2anc ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {e}=\left({{e}↾}_{\left(\left(0..^{S}+1\right)\setminus \left\{{S}\right\}\right)}\right)\cup \left\{⟨{S},{e}\left({S}\right)⟩\right\}$
101 12 66 eleqtrdi ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {S}\in {ℤ}_{\ge 0}$
102 fzodif2 ${⊢}{S}\in {ℤ}_{\ge 0}\to \left(0..^{S}+1\right)\setminus \left\{{S}\right\}=\left(0..^{S}\right)$
103 101 102 syl ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to \left(0..^{S}+1\right)\setminus \left\{{S}\right\}=\left(0..^{S}\right)$
104 103 reseq2d ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {{e}↾}_{\left(\left(0..^{S}+1\right)\setminus \left\{{S}\right\}\right)}={{e}↾}_{\left(0..^{S}\right)}$
105 104 uneq1d ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to \left({{e}↾}_{\left(\left(0..^{S}+1\right)\setminus \left\{{S}\right\}\right)}\right)\cup \left\{⟨{S},{e}\left({S}\right)⟩\right\}=\left({{e}↾}_{\left(0..^{S}\right)}\right)\cup \left\{⟨{S},{e}\left({S}\right)⟩\right\}$
106 100 105 eqtrd ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to {e}=\left({{e}↾}_{\left(0..^{S}\right)}\right)\cup \left\{⟨{S},{e}\left({S}\right)⟩\right\}$
107 94 97 106 rspcedvd ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to \exists {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{e}\left({S}\right)\right)\right)\phantom{\rule{.4em}{0ex}}{e}={c}\cup \left\{⟨{S},{e}\left({S}\right)⟩\right\}$
108 15 24 107 rspcedvd ${⊢}\left(\left({\phi }\wedge {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\to \exists {b}\in {A}\phantom{\rule{.4em}{0ex}}\exists {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\phantom{\rule{.4em}{0ex}}{e}={c}\cup \left\{⟨{S},{b}⟩\right\}$
109 108 anasss ${⊢}\left({\phi }\wedge \left({e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)\right)\to \exists {b}\in {A}\phantom{\rule{.4em}{0ex}}\exists {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\phantom{\rule{.4em}{0ex}}{e}={c}\cup \left\{⟨{S},{b}⟩\right\}$
110 simpr ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {e}={c}\cup \left\{⟨{S},{b}⟩\right\}$
111 1 adantr ${⊢}\left({\phi }\wedge {b}\in {A}\right)\to {A}\subseteq ℕ$
112 111 adantr ${⊢}\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\to {A}\subseteq ℕ$
113 2 adantr ${⊢}\left({\phi }\wedge {b}\in {A}\right)\to {M}\in ℤ$
114 89 sselda ${⊢}\left({\phi }\wedge {b}\in {A}\right)\to {b}\in ℤ$
115 113 114 zsubcld ${⊢}\left({\phi }\wedge {b}\in {A}\right)\to {M}-{b}\in ℤ$
116 115 adantr ${⊢}\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\to {M}-{b}\in ℤ$
117 3 adantr ${⊢}\left({\phi }\wedge {b}\in {A}\right)\to {S}\in {ℕ}_{0}$
118 117 adantr ${⊢}\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\to {S}\in {ℕ}_{0}$
119 simpr ${⊢}\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\to {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)$
120 112 116 118 119 reprf ${⊢}\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\to {c}:\left(0..^{S}\right)⟶{A}$
121 simplr ${⊢}\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\to {b}\in {A}$
122 118 121 fsnd ${⊢}\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\to \left\{⟨{S},{b}⟩\right\}:\left\{{S}\right\}⟶{A}$
123 fzodisjsn ${⊢}\left(0..^{S}\right)\cap \left\{{S}\right\}=\varnothing$
124 123 a1i ${⊢}\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\to \left(0..^{S}\right)\cap \left\{{S}\right\}=\varnothing$
125 120 122 124 fun2d ${⊢}\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\to \left({c}\cup \left\{⟨{S},{b}⟩\right\}\right):\left(0..^{S}\right)\cup \left\{{S}\right\}⟶{A}$
126 118 67 syl ${⊢}\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\to \left(0..^{S}+1\right)=\left(0..^{S}\right)\cup \left\{{S}\right\}$
127 126 feq2d ${⊢}\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\to \left(\left({c}\cup \left\{⟨{S},{b}⟩\right\}\right):\left(0..^{S}+1\right)⟶{A}↔\left({c}\cup \left\{⟨{S},{b}⟩\right\}\right):\left(0..^{S}\right)\cup \left\{{S}\right\}⟶{A}\right)$
128 125 127 mpbird ${⊢}\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\to \left({c}\cup \left\{⟨{S},{b}⟩\right\}\right):\left(0..^{S}+1\right)⟶{A}$
129 ovex ${⊢}\left(0..^{S}+1\right)\in \mathrm{V}$
130 elmapg ${⊢}\left({A}\in \mathrm{V}\wedge \left(0..^{S}+1\right)\in \mathrm{V}\right)\to \left({c}\cup \left\{⟨{S},{b}⟩\right\}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)↔\left({c}\cup \left\{⟨{S},{b}⟩\right\}\right):\left(0..^{S}+1\right)⟶{A}\right)$
131 33 129 130 sylancl ${⊢}{\phi }\to \left({c}\cup \left\{⟨{S},{b}⟩\right\}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)↔\left({c}\cup \left\{⟨{S},{b}⟩\right\}\right):\left(0..^{S}+1\right)⟶{A}\right)$
132 131 ad2antrr ${⊢}\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\to \left({c}\cup \left\{⟨{S},{b}⟩\right\}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)↔\left({c}\cup \left\{⟨{S},{b}⟩\right\}\right):\left(0..^{S}+1\right)⟶{A}\right)$
133 128 132 mpbird ${⊢}\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\to {c}\cup \left\{⟨{S},{b}⟩\right\}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)$
134 133 adantr ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {c}\cup \left\{⟨{S},{b}⟩\right\}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)$
135 110 134 eqeltrd ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)$
136 126 adantr ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \left(0..^{S}+1\right)=\left(0..^{S}\right)\cup \left\{{S}\right\}$
137 136 sumeq1d ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)=\sum _{{a}\in \left(0..^{S}\right)\cup \left\{{S}\right\}}{e}\left({a}\right)$
138 nfv ${⊢}Ⅎ{a}\phantom{\rule{.4em}{0ex}}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)$
139 34 a1i ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \left(0..^{S}\right)\in \mathrm{Fin}$
140 118 adantr ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {S}\in {ℕ}_{0}$
141 57 a1i ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to ¬{S}\in \left(0..^{S}\right)$
142 43 ad4antr ${⊢}\left(\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {A}\subseteq ℂ$
143 128 adantr ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \left({c}\cup \left\{⟨{S},{b}⟩\right\}\right):\left(0..^{S}+1\right)⟶{A}$
144 110 feq1d ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \left({e}:\left(0..^{S}+1\right)⟶{A}↔\left({c}\cup \left\{⟨{S},{b}⟩\right\}\right):\left(0..^{S}+1\right)⟶{A}\right)$
145 143 144 mpbird ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {e}:\left(0..^{S}+1\right)⟶{A}$
146 145 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {e}:\left(0..^{S}+1\right)⟶{A}$
147 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {a}\in \left(0..^{S}\right)$
148 elun1 ${⊢}{a}\in \left(0..^{S}\right)\to {a}\in \left(\left(0..^{S}\right)\cup \left\{{S}\right\}\right)$
149 147 148 syl ${⊢}\left(\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {a}\in \left(\left(0..^{S}\right)\cup \left\{{S}\right\}\right)$
150 126 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\wedge {a}\in \left(0..^{S}\right)\right)\to \left(0..^{S}+1\right)=\left(0..^{S}\right)\cup \left\{{S}\right\}$
151 149 150 eleqtrrd ${⊢}\left(\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {a}\in \left(0..^{S}+1\right)$
152 146 151 ffvelrnd ${⊢}\left(\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {e}\left({a}\right)\in {A}$
153 142 152 sseldd ${⊢}\left(\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {e}\left({a}\right)\in ℂ$
154 43 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {A}\subseteq ℂ$
155 140 13 syl ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {S}\in \left(0..^{S}+1\right)$
156 145 155 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {e}\left({S}\right)\in {A}$
157 154 156 sseldd ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {e}\left({S}\right)\in ℂ$
158 138 56 139 140 141 153 63 157 fsumsplitsn ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \sum _{{a}\in \left(0..^{S}\right)\cup \left\{{S}\right\}}{e}\left({a}\right)=\sum _{{a}\in \left(0..^{S}\right)}{e}\left({a}\right)+{e}\left({S}\right)$
159 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {e}={c}\cup \left\{⟨{S},{b}⟩\right\}$
160 159 fveq1d ${⊢}\left(\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {e}\left({a}\right)=\left({c}\cup \left\{⟨{S},{b}⟩\right\}\right)\left({a}\right)$
161 120 ffnd ${⊢}\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\to {c}Fn\left(0..^{S}\right)$
162 161 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {c}Fn\left(0..^{S}\right)$
163 122 ffnd ${⊢}\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\to \left\{⟨{S},{b}⟩\right\}Fn\left\{{S}\right\}$
164 163 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\wedge {a}\in \left(0..^{S}\right)\right)\to \left\{⟨{S},{b}⟩\right\}Fn\left\{{S}\right\}$
165 123 a1i ${⊢}\left(\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\wedge {a}\in \left(0..^{S}\right)\right)\to \left(0..^{S}\right)\cap \left\{{S}\right\}=\varnothing$
166 fvun1 ${⊢}\left({c}Fn\left(0..^{S}\right)\wedge \left\{⟨{S},{b}⟩\right\}Fn\left\{{S}\right\}\wedge \left(\left(0..^{S}\right)\cap \left\{{S}\right\}=\varnothing \wedge {a}\in \left(0..^{S}\right)\right)\right)\to \left({c}\cup \left\{⟨{S},{b}⟩\right\}\right)\left({a}\right)={c}\left({a}\right)$
167 162 164 165 147 166 syl112anc ${⊢}\left(\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\wedge {a}\in \left(0..^{S}\right)\right)\to \left({c}\cup \left\{⟨{S},{b}⟩\right\}\right)\left({a}\right)={c}\left({a}\right)$
168 160 167 eqtrd ${⊢}\left(\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\wedge {a}\in \left(0..^{S}\right)\right)\to {e}\left({a}\right)={c}\left({a}\right)$
169 168 ralrimiva ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \forall {a}\in \left(0..^{S}\right)\phantom{\rule{.4em}{0ex}}{e}\left({a}\right)={c}\left({a}\right)$
170 169 sumeq2d ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \sum _{{a}\in \left(0..^{S}\right)}{e}\left({a}\right)=\sum _{{a}\in \left(0..^{S}\right)}{c}\left({a}\right)$
171 112 adantr ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {A}\subseteq ℕ$
172 116 adantr ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {M}-{b}\in ℤ$
173 119 adantr ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)$
174 171 172 140 173 reprsum ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \sum _{{a}\in \left(0..^{S}\right)}{c}\left({a}\right)={M}-{b}$
175 170 174 eqtrd ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \sum _{{a}\in \left(0..^{S}\right)}{e}\left({a}\right)={M}-{b}$
176 110 fveq1d ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {e}\left({S}\right)=\left({c}\cup \left\{⟨{S},{b}⟩\right\}\right)\left({S}\right)$
177 161 adantr ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {c}Fn\left(0..^{S}\right)$
178 163 adantr ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \left\{⟨{S},{b}⟩\right\}Fn\left\{{S}\right\}$
179 123 a1i ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \left(0..^{S}\right)\cap \left\{{S}\right\}=\varnothing$
180 snidg ${⊢}{S}\in {ℕ}_{0}\to {S}\in \left\{{S}\right\}$
181 140 180 syl ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {S}\in \left\{{S}\right\}$
182 fvun2 ${⊢}\left({c}Fn\left(0..^{S}\right)\wedge \left\{⟨{S},{b}⟩\right\}Fn\left\{{S}\right\}\wedge \left(\left(0..^{S}\right)\cap \left\{{S}\right\}=\varnothing \wedge {S}\in \left\{{S}\right\}\right)\right)\to \left({c}\cup \left\{⟨{S},{b}⟩\right\}\right)\left({S}\right)=\left\{⟨{S},{b}⟩\right\}\left({S}\right)$
183 177 178 179 181 182 syl112anc ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \left({c}\cup \left\{⟨{S},{b}⟩\right\}\right)\left({S}\right)=\left\{⟨{S},{b}⟩\right\}\left({S}\right)$
184 121 adantr ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {b}\in {A}$
185 fvsng ${⊢}\left({S}\in {ℕ}_{0}\wedge {b}\in {A}\right)\to \left\{⟨{S},{b}⟩\right\}\left({S}\right)={b}$
186 140 184 185 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \left\{⟨{S},{b}⟩\right\}\left({S}\right)={b}$
187 176 183 186 3eqtrd ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {e}\left({S}\right)={b}$
188 175 187 oveq12d ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \sum _{{a}\in \left(0..^{S}\right)}{e}\left({a}\right)+{e}\left({S}\right)={M}-{b}+{b}$
189 zsscn ${⊢}ℤ\subseteq ℂ$
190 113 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {M}\in ℤ$
191 189 190 sseldi ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {M}\in ℂ$
192 187 157 eqeltrrd ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {b}\in ℂ$
193 191 192 npcand ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to {M}-{b}+{b}={M}$
194 188 193 eqtrd ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \sum _{{a}\in \left(0..^{S}\right)}{e}\left({a}\right)+{e}\left({S}\right)={M}$
195 137 158 194 3eqtrd ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}$
196 135 195 jca ${⊢}\left(\left(\left({\phi }\wedge {b}\in {A}\right)\wedge {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\right)\wedge {e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \left({e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)$
197 196 r19.29ffa ${⊢}\left({\phi }\wedge \exists {b}\in {A}\phantom{\rule{.4em}{0ex}}\exists {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\phantom{\rule{.4em}{0ex}}{e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)\to \left({e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)$
198 109 197 impbida ${⊢}{\phi }\to \left(\left({e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)↔\exists {b}\in {A}\phantom{\rule{.4em}{0ex}}\exists {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\phantom{\rule{.4em}{0ex}}{e}={c}\cup \left\{⟨{S},{b}⟩\right\}\right)$
199 vex ${⊢}{c}\in \mathrm{V}$
200 snex ${⊢}\left\{⟨{S},{b}⟩\right\}\in \mathrm{V}$
201 199 200 unex ${⊢}{c}\cup \left\{⟨{S},{b}⟩\right\}\in \mathrm{V}$
202 4 201 elrnmpti ${⊢}{e}\in \mathrm{ran}{F}↔\exists {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\phantom{\rule{.4em}{0ex}}{e}={c}\cup \left\{⟨{S},{b}⟩\right\}$
203 202 rexbii ${⊢}\exists {b}\in {A}\phantom{\rule{.4em}{0ex}}{e}\in \mathrm{ran}{F}↔\exists {b}\in {A}\phantom{\rule{.4em}{0ex}}\exists {c}\in \left({A}\mathrm{repr}\left({S}\right)\left({M}-{b}\right)\right)\phantom{\rule{.4em}{0ex}}{e}={c}\cup \left\{⟨{S},{b}⟩\right\}$
204 198 203 syl6bbr ${⊢}{\phi }\to \left(\left({e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)↔\exists {b}\in {A}\phantom{\rule{.4em}{0ex}}{e}\in \mathrm{ran}{F}\right)$
205 fveq1 ${⊢}{c}={e}\to {c}\left({a}\right)={e}\left({a}\right)$
206 205 sumeq2sdv ${⊢}{c}={e}\to \sum _{{a}\in \left(0..^{S}+1\right)}{c}\left({a}\right)=\sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)$
207 206 eqeq1d ${⊢}{c}={e}\to \left(\sum _{{a}\in \left(0..^{S}+1\right)}{c}\left({a}\right)={M}↔\sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)$
208 207 cbvrabv ${⊢}\left\{{c}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)|\sum _{{a}\in \left(0..^{S}+1\right)}{c}\left({a}\right)={M}\right\}=\left\{{e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)|\sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right\}$
209 208 rabeq2i ${⊢}{e}\in \left\{{c}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)|\sum _{{a}\in \left(0..^{S}+1\right)}{c}\left({a}\right)={M}\right\}↔\left({e}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)\wedge \sum _{{a}\in \left(0..^{S}+1\right)}{e}\left({a}\right)={M}\right)$
210 eliun ${⊢}{e}\in \bigcup _{{b}\in {A}}\mathrm{ran}{F}↔\exists {b}\in {A}\phantom{\rule{.4em}{0ex}}{e}\in \mathrm{ran}{F}$
211 204 209 210 3bitr4g ${⊢}{\phi }\to \left({e}\in \left\{{c}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)|\sum _{{a}\in \left(0..^{S}+1\right)}{c}\left({a}\right)={M}\right\}↔{e}\in \bigcup _{{b}\in {A}}\mathrm{ran}{F}\right)$
212 211 eqrdv ${⊢}{\phi }\to \left\{{c}\in \left({{A}}^{\left(0..^{S}+1\right)}\right)|\sum _{{a}\in \left(0..^{S}+1\right)}{c}\left({a}\right)={M}\right\}=\bigcup _{{b}\in {A}}\mathrm{ran}{F}$
213 8 212 eqtrd ${⊢}{\phi }\to {A}\mathrm{repr}\left({S}+1\right){M}=\bigcup _{{b}\in {A}}\mathrm{ran}{F}$