# Metamath Proof Explorer

## Theorem poimirlem4

Description: Lemma for poimir connecting the admissible faces on the back face of the ( M + 1 ) -cube to admissible simplices in the M -cube. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 ${⊢}{\phi }\to {N}\in ℕ$
poimirlem4.1 ${⊢}{\phi }\to {K}\in ℕ$
poimirlem4.2 ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
poimirlem4.3 ${⊢}{\phi }\to {M}<{N}$
Assertion poimirlem4

### Proof

Step Hyp Ref Expression
1 poimir.0 ${⊢}{\phi }\to {N}\in ℕ$
2 poimirlem4.1 ${⊢}{\phi }\to {K}\in ℕ$
3 poimirlem4.2 ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
4 poimirlem4.3 ${⊢}{\phi }\to {M}<{N}$
5 1 adantr ${⊢}\left({\phi }\wedge {t}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}\right)\right)\to {N}\in ℕ$
6 2 adantr ${⊢}\left({\phi }\wedge {t}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}\right)\right)\to {K}\in ℕ$
7 3 adantr ${⊢}\left({\phi }\wedge {t}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}\right)\right)\to {M}\in {ℕ}_{0}$
8 4 adantr ${⊢}\left({\phi }\wedge {t}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}\right)\right)\to {M}<{N}$
9 xp1st ${⊢}{t}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}\right)\to {1}^{st}\left({t}\right)\in \left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)$
10 elmapi ${⊢}{1}^{st}\left({t}\right)\in \left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)\to {1}^{st}\left({t}\right):\left(1\dots {M}\right)⟶\left(0..^{K}\right)$
11 9 10 syl ${⊢}{t}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}\right)\to {1}^{st}\left({t}\right):\left(1\dots {M}\right)⟶\left(0..^{K}\right)$
12 11 adantl ${⊢}\left({\phi }\wedge {t}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}\right)\right)\to {1}^{st}\left({t}\right):\left(1\dots {M}\right)⟶\left(0..^{K}\right)$
13 xp2nd ${⊢}{t}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}\right)\to {2}^{nd}\left({t}\right)\in \left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}$
14 fvex ${⊢}{2}^{nd}\left({t}\right)\in \mathrm{V}$
15 f1oeq1 ${⊢}{f}={2}^{nd}\left({t}\right)\to \left({f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)↔{2}^{nd}\left({t}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right)$
16 14 15 elab ${⊢}{2}^{nd}\left({t}\right)\in \left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}↔{2}^{nd}\left({t}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)$
17 13 16 sylib ${⊢}{t}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}\right)\to {2}^{nd}\left({t}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)$
18 17 adantl ${⊢}\left({\phi }\wedge {t}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}\right)\right)\to {2}^{nd}\left({t}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)$
19 5 6 7 8 12 18 poimirlem3
20 fvex ${⊢}{1}^{st}\left({t}\right)\in \mathrm{V}$
21 snex ${⊢}\left\{⟨{M}+1,0⟩\right\}\in \mathrm{V}$
22 20 21 unex ${⊢}{1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\}\in \mathrm{V}$
23 snex ${⊢}\left\{⟨{M}+1,{M}+1⟩\right\}\in \mathrm{V}$
24 14 23 unex ${⊢}{2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}\in \mathrm{V}$
25 22 24 op1std ${⊢}{s}=⟨{1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\},{2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}⟩\to {1}^{st}\left({s}\right)={1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\}$
26 22 24 op2ndd ${⊢}{s}=⟨{1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\},{2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}⟩\to {2}^{nd}\left({s}\right)={2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}$
27 26 imaeq1d ${⊢}{s}=⟨{1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\},{2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}⟩\to {2}^{nd}\left({s}\right)\left[\left(1\dots {j}\right)\right]=\left({2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}\right)\left[\left(1\dots {j}\right)\right]$
28 27 xpeq1d ${⊢}{s}=⟨{1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\},{2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}⟩\to {2}^{nd}\left({s}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}=\left({2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}$
29 26 imaeq1d ${⊢}{s}=⟨{1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\},{2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}⟩\to {2}^{nd}\left({s}\right)\left[\left({j}+1\dots {M}+1\right)\right]=\left({2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}\right)\left[\left({j}+1\dots {M}+1\right)\right]$
30 29 xpeq1d ${⊢}{s}=⟨{1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\},{2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}⟩\to {2}^{nd}\left({s}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}=\left({2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}$
31 28 30 uneq12d ${⊢}{s}=⟨{1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\},{2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}⟩\to \left({2}^{nd}\left({s}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({s}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)=\left(\left({2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left(\left({2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)$
32 25 31 oveq12d ${⊢}{s}=⟨{1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\},{2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}⟩\to {1}^{st}\left({s}\right){+}_{f}\left(\left({2}^{nd}\left({s}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({s}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)=\left({1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\}\right){+}_{f}\left(\left(\left({2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left(\left({2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)$
33 32 uneq1d ${⊢}{s}=⟨{1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\},{2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}⟩\to \left({1}^{st}\left({s}\right){+}_{f}\left(\left({2}^{nd}\left({s}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({s}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\right)\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)=\left(\left({1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\}\right){+}_{f}\left(\left(\left({2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left(\left({2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\right)\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)$
34 33 csbeq1d
35 34 eqeq2d
36 35 rexbidv
37 36 ralbidv
38 25 fveq1d ${⊢}{s}=⟨{1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\},{2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}⟩\to {1}^{st}\left({s}\right)\left({M}+1\right)=\left({1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\}\right)\left({M}+1\right)$
39 38 eqeq1d ${⊢}{s}=⟨{1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\},{2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}⟩\to \left({1}^{st}\left({s}\right)\left({M}+1\right)=0↔\left({1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\}\right)\left({M}+1\right)=0\right)$
40 26 fveq1d ${⊢}{s}=⟨{1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\},{2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}⟩\to {2}^{nd}\left({s}\right)\left({M}+1\right)=\left({2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}\right)\left({M}+1\right)$
41 40 eqeq1d ${⊢}{s}=⟨{1}^{st}\left({t}\right)\cup \left\{⟨{M}+1,0⟩\right\},{2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}⟩\to \left({2}^{nd}\left({s}\right)\left({M}+1\right)={M}+1↔\left({2}^{nd}\left({t}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}\right)\left({M}+1\right)={M}+1\right)$
42 37 39 41 3anbi123d
43 42 elrab
44 19 43 syl6ibr
45 44 ralrimiva
46 fveq2 ${⊢}{s}={t}\to {1}^{st}\left({s}\right)={1}^{st}\left({t}\right)$
47 fveq2 ${⊢}{s}={t}\to {2}^{nd}\left({s}\right)={2}^{nd}\left({t}\right)$
48 47 imaeq1d ${⊢}{s}={t}\to {2}^{nd}\left({s}\right)\left[\left(1\dots {j}\right)\right]={2}^{nd}\left({t}\right)\left[\left(1\dots {j}\right)\right]$
49 48 xpeq1d ${⊢}{s}={t}\to {2}^{nd}\left({s}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}={2}^{nd}\left({t}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}$
50 47 imaeq1d ${⊢}{s}={t}\to {2}^{nd}\left({s}\right)\left[\left({j}+1\dots {M}\right)\right]={2}^{nd}\left({t}\right)\left[\left({j}+1\dots {M}\right)\right]$
51 50 xpeq1d ${⊢}{s}={t}\to {2}^{nd}\left({s}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}={2}^{nd}\left({t}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}$
52 49 51 uneq12d ${⊢}{s}={t}\to \left({2}^{nd}\left({s}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({s}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)=\left({2}^{nd}\left({t}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({t}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)$
53 46 52 oveq12d ${⊢}{s}={t}\to {1}^{st}\left({s}\right){+}_{f}\left(\left({2}^{nd}\left({s}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({s}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)={1}^{st}\left({t}\right){+}_{f}\left(\left({2}^{nd}\left({t}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({t}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)$
54 53 uneq1d ${⊢}{s}={t}\to \left({1}^{st}\left({s}\right){+}_{f}\left(\left({2}^{nd}\left({s}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({s}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\right)\cup \left(\left({M}+1\dots {N}\right)×\left\{0\right\}\right)=\left({1}^{st}\left({t}\right){+}_{f}\left(\left({2}^{nd}\left({t}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({t}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\right)\cup \left(\left({M}+1\dots {N}\right)×\left\{0\right\}\right)$
55 54 csbeq1d
56 55 eqeq2d
57 56 rexbidv
58 57 ralbidv
59 58 ralrab
60 45 59 sylibr
61 xp1st ${⊢}{k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\to {1}^{st}\left({k}\right)\in \left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)$
62 elmapi ${⊢}{1}^{st}\left({k}\right)\in \left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)\to {1}^{st}\left({k}\right):\left(1\dots {M}+1\right)⟶\left(0..^{K}\right)$
63 61 62 syl ${⊢}{k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\to {1}^{st}\left({k}\right):\left(1\dots {M}+1\right)⟶\left(0..^{K}\right)$
64 fzssp1 ${⊢}\left(1\dots {M}\right)\subseteq \left(1\dots {M}+1\right)$
65 fssres ${⊢}\left({1}^{st}\left({k}\right):\left(1\dots {M}+1\right)⟶\left(0..^{K}\right)\wedge \left(1\dots {M}\right)\subseteq \left(1\dots {M}+1\right)\right)\to \left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right):\left(1\dots {M}\right)⟶\left(0..^{K}\right)$
66 63 64 65 sylancl ${⊢}{k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\to \left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right):\left(1\dots {M}\right)⟶\left(0..^{K}\right)$
67 ovex ${⊢}\left(0..^{K}\right)\in \mathrm{V}$
68 ovex ${⊢}\left(1\dots {M}\right)\in \mathrm{V}$
69 67 68 elmap ${⊢}{{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\in \left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)↔\left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right):\left(1\dots {M}\right)⟶\left(0..^{K}\right)$
70 66 69 sylibr ${⊢}{k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\to {{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\in \left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)$
71 70 ad2antlr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to {{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\in \left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)$
72 xp2nd ${⊢}{k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\to {2}^{nd}\left({k}\right)\in \left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}$
73 fvex ${⊢}{2}^{nd}\left({k}\right)\in \mathrm{V}$
74 f1oeq1 ${⊢}{f}={2}^{nd}\left({k}\right)\to \left({f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)↔{2}^{nd}\left({k}\right):\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right)$
75 73 74 elab ${⊢}{2}^{nd}\left({k}\right)\in \left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}↔{2}^{nd}\left({k}\right):\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)$
76 72 75 sylib ${⊢}{k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\to {2}^{nd}\left({k}\right):\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)$
77 f1of1 ${⊢}{2}^{nd}\left({k}\right):\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\to {2}^{nd}\left({k}\right):\left(1\dots {M}+1\right)\underset{1-1}{⟶}\left(1\dots {M}+1\right)$
78 76 77 syl ${⊢}{k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\to {2}^{nd}\left({k}\right):\left(1\dots {M}+1\right)\underset{1-1}{⟶}\left(1\dots {M}+1\right)$
79 f1ores ${⊢}\left({2}^{nd}\left({k}\right):\left(1\dots {M}+1\right)\underset{1-1}{⟶}\left(1\dots {M}+1\right)\wedge \left(1\dots {M}\right)\subseteq \left(1\dots {M}+1\right)\right)\to \left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}{2}^{nd}\left({k}\right)\left[\left(1\dots {M}\right)\right]$
80 78 64 79 sylancl ${⊢}{k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\to \left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}{2}^{nd}\left({k}\right)\left[\left(1\dots {M}\right)\right]$
81 80 ad2antlr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to \left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}{2}^{nd}\left({k}\right)\left[\left(1\dots {M}\right)\right]$
82 dff1o3 ${⊢}{2}^{nd}\left({k}\right):\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)↔\left({2}^{nd}\left({k}\right):\left(1\dots {M}+1\right)\underset{onto}{⟶}\left(1\dots {M}+1\right)\wedge \mathrm{Fun}{{2}^{nd}\left({k}\right)}^{-1}\right)$
83 82 simprbi ${⊢}{2}^{nd}\left({k}\right):\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\to \mathrm{Fun}{{2}^{nd}\left({k}\right)}^{-1}$
84 imadif ${⊢}\mathrm{Fun}{{2}^{nd}\left({k}\right)}^{-1}\to {2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\right]\setminus {2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]$
85 76 83 84 3syl ${⊢}{k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\right]\setminus {2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]$
86 85 ad2antlr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\right]\setminus {2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]$
87 f1ofo ${⊢}{2}^{nd}\left({k}\right):\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\to {2}^{nd}\left({k}\right):\left(1\dots {M}+1\right)\underset{onto}{⟶}\left(1\dots {M}+1\right)$
88 foima ${⊢}{2}^{nd}\left({k}\right):\left(1\dots {M}+1\right)\underset{onto}{⟶}\left(1\dots {M}+1\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\right]=\left(1\dots {M}+1\right)$
89 76 87 88 3syl ${⊢}{k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\right]=\left(1\dots {M}+1\right)$
90 89 ad2antlr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\right]=\left(1\dots {M}+1\right)$
91 f1ofn ${⊢}{2}^{nd}\left({k}\right):\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\to {2}^{nd}\left({k}\right)Fn\left(1\dots {M}+1\right)$
92 76 91 syl ${⊢}{k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\to {2}^{nd}\left({k}\right)Fn\left(1\dots {M}+1\right)$
93 nn0p1nn ${⊢}{M}\in {ℕ}_{0}\to {M}+1\in ℕ$
94 3 93 syl ${⊢}{\phi }\to {M}+1\in ℕ$
95 elfz1end ${⊢}{M}+1\in ℕ↔{M}+1\in \left(1\dots {M}+1\right)$
96 94 95 sylib ${⊢}{\phi }\to {M}+1\in \left(1\dots {M}+1\right)$
97 fnsnfv ${⊢}\left({2}^{nd}\left({k}\right)Fn\left(1\dots {M}+1\right)\wedge {M}+1\in \left(1\dots {M}+1\right)\right)\to \left\{{2}^{nd}\left({k}\right)\left({M}+1\right)\right\}={2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]$
98 92 96 97 syl2anr ${⊢}\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\to \left\{{2}^{nd}\left({k}\right)\left({M}+1\right)\right\}={2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]$
99 sneq ${⊢}{2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\to \left\{{2}^{nd}\left({k}\right)\left({M}+1\right)\right\}=\left\{{M}+1\right\}$
100 98 99 sylan9req ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to {2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]=\left\{{M}+1\right\}$
101 90 100 difeq12d ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\right]\setminus {2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]=\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}$
102 86 101 eqtrd ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right]=\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}$
103 1z ${⊢}1\in ℤ$
104 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
105 1m1e0 ${⊢}1-1=0$
106 105 fveq2i ${⊢}{ℤ}_{\ge \left(1-1\right)}={ℤ}_{\ge 0}$
107 104 106 eqtr4i ${⊢}{ℕ}_{0}={ℤ}_{\ge \left(1-1\right)}$
108 3 107 eleqtrdi ${⊢}{\phi }\to {M}\in {ℤ}_{\ge \left(1-1\right)}$
109 fzsuc2 ${⊢}\left(1\in ℤ\wedge {M}\in {ℤ}_{\ge \left(1-1\right)}\right)\to \left(1\dots {M}+1\right)=\left(1\dots {M}\right)\cup \left\{{M}+1\right\}$
110 103 108 109 sylancr ${⊢}{\phi }\to \left(1\dots {M}+1\right)=\left(1\dots {M}\right)\cup \left\{{M}+1\right\}$
111 110 difeq1d ${⊢}{\phi }\to \left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}=\left(\left(1\dots {M}\right)\cup \left\{{M}+1\right\}\right)\setminus \left\{{M}+1\right\}$
112 difun2 ${⊢}\left(\left(1\dots {M}\right)\cup \left\{{M}+1\right\}\right)\setminus \left\{{M}+1\right\}=\left(1\dots {M}\right)\setminus \left\{{M}+1\right\}$
113 111 112 syl6eq ${⊢}{\phi }\to \left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}=\left(1\dots {M}\right)\setminus \left\{{M}+1\right\}$
114 3 nn0red ${⊢}{\phi }\to {M}\in ℝ$
115 ltp1 ${⊢}{M}\in ℝ\to {M}<{M}+1$
116 peano2re ${⊢}{M}\in ℝ\to {M}+1\in ℝ$
117 ltnle ${⊢}\left({M}\in ℝ\wedge {M}+1\in ℝ\right)\to \left({M}<{M}+1↔¬{M}+1\le {M}\right)$
118 116 117 mpdan ${⊢}{M}\in ℝ\to \left({M}<{M}+1↔¬{M}+1\le {M}\right)$
119 115 118 mpbid ${⊢}{M}\in ℝ\to ¬{M}+1\le {M}$
120 114 119 syl ${⊢}{\phi }\to ¬{M}+1\le {M}$
121 elfzle2 ${⊢}{M}+1\in \left(1\dots {M}\right)\to {M}+1\le {M}$
122 120 121 nsyl ${⊢}{\phi }\to ¬{M}+1\in \left(1\dots {M}\right)$
123 difsn ${⊢}¬{M}+1\in \left(1\dots {M}\right)\to \left(1\dots {M}\right)\setminus \left\{{M}+1\right\}=\left(1\dots {M}\right)$
124 122 123 syl ${⊢}{\phi }\to \left(1\dots {M}\right)\setminus \left\{{M}+1\right\}=\left(1\dots {M}\right)$
125 113 124 eqtrd ${⊢}{\phi }\to \left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}=\left(1\dots {M}\right)$
126 125 imaeq2d ${⊢}{\phi }\to {2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {M}\right)\right]$
127 126 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {M}\right)\right]$
128 125 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to \left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}=\left(1\dots {M}\right)$
129 102 127 128 3eqtr3d ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {M}\right)\right]=\left(1\dots {M}\right)$
130 f1oeq3 ${⊢}{2}^{nd}\left({k}\right)\left[\left(1\dots {M}\right)\right]=\left(1\dots {M}\right)\to \left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}{2}^{nd}\left({k}\right)\left[\left(1\dots {M}\right)\right]↔\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right)$
131 129 130 syl ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to \left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}{2}^{nd}\left({k}\right)\left[\left(1\dots {M}\right)\right]↔\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right)$
132 81 131 mpbid ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to \left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)$
133 73 resex ${⊢}{{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\in \mathrm{V}$
134 f1oeq1 ${⊢}{f}={{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\to \left({f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)↔\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right)$
135 133 134 elab ${⊢}{{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\in \left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}↔\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)$
136 132 135 sylibr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to {{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\in \left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}$
137 opelxpi ${⊢}\left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\in \left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)\wedge {{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\in \left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}\right)\to ⟨{{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)},{{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}⟩\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}\right)$
138 71 136 137 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to ⟨{{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)},{{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}⟩\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right\}\right)$
140 3anass
141 ancom
142 140 141 bitri
143 94 nnzd ${⊢}{\phi }\to {M}+1\in ℤ$
144 uzid ${⊢}{M}+1\in ℤ\to {M}+1\in {ℤ}_{\ge \left({M}+1\right)}$
145 peano2uz ${⊢}{M}+1\in {ℤ}_{\ge \left({M}+1\right)}\to {M}+1+1\in {ℤ}_{\ge \left({M}+1\right)}$
146 143 144 145 3syl ${⊢}{\phi }\to {M}+1+1\in {ℤ}_{\ge \left({M}+1\right)}$
147 3 nn0zd ${⊢}{\phi }\to {M}\in ℤ$
148 1 nnzd ${⊢}{\phi }\to {N}\in ℤ$
149 zltp1le ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}<{N}↔{M}+1\le {N}\right)$
150 peano2z ${⊢}{M}\in ℤ\to {M}+1\in ℤ$
151 eluz ${⊢}\left({M}+1\in ℤ\wedge {N}\in ℤ\right)\to \left({N}\in {ℤ}_{\ge \left({M}+1\right)}↔{M}+1\le {N}\right)$
152 150 151 sylan ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({N}\in {ℤ}_{\ge \left({M}+1\right)}↔{M}+1\le {N}\right)$
153 149 152 bitr4d ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}<{N}↔{N}\in {ℤ}_{\ge \left({M}+1\right)}\right)$
154 147 148 153 syl2anc ${⊢}{\phi }\to \left({M}<{N}↔{N}\in {ℤ}_{\ge \left({M}+1\right)}\right)$
155 4 154 mpbid ${⊢}{\phi }\to {N}\in {ℤ}_{\ge \left({M}+1\right)}$
156 fzsplit2 ${⊢}\left({M}+1+1\in {ℤ}_{\ge \left({M}+1\right)}\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to \left({M}+1\dots {N}\right)=\left({M}+1\dots {M}+1\right)\cup \left({M}+1+1\dots {N}\right)$
157 146 155 156 syl2anc ${⊢}{\phi }\to \left({M}+1\dots {N}\right)=\left({M}+1\dots {M}+1\right)\cup \left({M}+1+1\dots {N}\right)$
158 fzsn ${⊢}{M}+1\in ℤ\to \left({M}+1\dots {M}+1\right)=\left\{{M}+1\right\}$
159 143 158 syl ${⊢}{\phi }\to \left({M}+1\dots {M}+1\right)=\left\{{M}+1\right\}$
160 159 uneq1d ${⊢}{\phi }\to \left({M}+1\dots {M}+1\right)\cup \left({M}+1+1\dots {N}\right)=\left\{{M}+1\right\}\cup \left({M}+1+1\dots {N}\right)$
161 157 160 eqtrd ${⊢}{\phi }\to \left({M}+1\dots {N}\right)=\left\{{M}+1\right\}\cup \left({M}+1+1\dots {N}\right)$
162 161 xpeq1d ${⊢}{\phi }\to \left({M}+1\dots {N}\right)×\left\{0\right\}=\left(\left\{{M}+1\right\}\cup \left({M}+1+1\dots {N}\right)\right)×\left\{0\right\}$
163 162 uneq2d ${⊢}{\phi }\to \left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left(\left({M}+1\dots {N}\right)×\left\{0\right\}\right)=\left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left(\left(\left\{{M}+1\right\}\cup \left({M}+1+1\dots {N}\right)\right)×\left\{0\right\}\right)$
164 xpundir ${⊢}\left(\left\{{M}+1\right\}\cup \left({M}+1+1\dots {N}\right)\right)×\left\{0\right\}=\left(\left\{{M}+1\right\}×\left\{0\right\}\right)\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)$
165 ovex ${⊢}{M}+1\in \mathrm{V}$
166 c0ex ${⊢}0\in \mathrm{V}$
167 165 166 xpsn ${⊢}\left\{{M}+1\right\}×\left\{0\right\}=\left\{⟨{M}+1,0⟩\right\}$
168 167 uneq1i ${⊢}\left(\left\{{M}+1\right\}×\left\{0\right\}\right)\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)=\left\{⟨{M}+1,0⟩\right\}\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)$
169 164 168 eqtri ${⊢}\left(\left\{{M}+1\right\}\cup \left({M}+1+1\dots {N}\right)\right)×\left\{0\right\}=\left\{⟨{M}+1,0⟩\right\}\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)$
170 169 uneq2i ${⊢}\left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left(\left(\left\{{M}+1\right\}\cup \left({M}+1+1\dots {N}\right)\right)×\left\{0\right\}\right)=\left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left(\left\{⟨{M}+1,0⟩\right\}\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)\right)$
171 unass ${⊢}\left(\left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left\{⟨{M}+1,0⟩\right\}\right)\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)=\left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left(\left\{⟨{M}+1,0⟩\right\}\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)\right)$
172 170 171 eqtr4i ${⊢}\left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left(\left(\left\{{M}+1\right\}\cup \left({M}+1+1\dots {N}\right)\right)×\left\{0\right\}\right)=\left(\left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left\{⟨{M}+1,0⟩\right\}\right)\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)$
173 163 172 syl6eq ${⊢}{\phi }\to \left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left(\left({M}+1\dots {N}\right)×\left\{0\right\}\right)=\left(\left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left\{⟨{M}+1,0⟩\right\}\right)\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)$
174 173 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left(\left({M}+1\dots {N}\right)×\left\{0\right\}\right)=\left(\left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left\{⟨{M}+1,0⟩\right\}\right)\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)$
175 165 a1i ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {M}+1\in \mathrm{V}$
176 166 a1i ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to 0\in \mathrm{V}$
177 110 eqcomd ${⊢}{\phi }\to \left(1\dots {M}\right)\cup \left\{{M}+1\right\}=\left(1\dots {M}+1\right)$
178 177 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(1\dots {M}\right)\cup \left\{{M}+1\right\}=\left(1\dots {M}+1\right)$
179 fveq2 ${⊢}{n}={M}+1\to {1}^{st}\left({k}\right)\left({n}\right)={1}^{st}\left({k}\right)\left({M}+1\right)$
180 fveq2 ${⊢}{n}={M}+1\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({M}+1\right)$
181 179 180 oveq12d ${⊢}{n}={M}+1\to {1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)={1}^{st}\left({k}\right)\left({M}+1\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({M}+1\right)$
182 simplrl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {1}^{st}\left({k}\right)\left({M}+1\right)=0$
183 imain ${⊢}\mathrm{Fun}{{2}^{nd}\left({k}\right)}^{-1}\to {2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\cap \left({j}+1\dots {M}+1\right)\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cap {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]$
184 76 83 183 3syl ${⊢}{k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\cap \left({j}+1\dots {M}+1\right)\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cap {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]$
185 184 ad2antlr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\cap \left({j}+1\dots {M}+1\right)\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cap {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]$
186 elfznn0 ${⊢}{j}\in \left(0\dots {M}\right)\to {j}\in {ℕ}_{0}$
187 186 nn0red ${⊢}{j}\in \left(0\dots {M}\right)\to {j}\in ℝ$
188 187 ltp1d ${⊢}{j}\in \left(0\dots {M}\right)\to {j}<{j}+1$
189 fzdisj ${⊢}{j}<{j}+1\to \left(1\dots {j}\right)\cap \left({j}+1\dots {M}+1\right)=\varnothing$
190 188 189 syl ${⊢}{j}\in \left(0\dots {M}\right)\to \left(1\dots {j}\right)\cap \left({j}+1\dots {M}+1\right)=\varnothing$
191 190 imaeq2d ${⊢}{j}\in \left(0\dots {M}\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\cap \left({j}+1\dots {M}+1\right)\right]={2}^{nd}\left({k}\right)\left[\varnothing \right]$
192 ima0 ${⊢}{2}^{nd}\left({k}\right)\left[\varnothing \right]=\varnothing$
193 191 192 syl6eq ${⊢}{j}\in \left(0\dots {M}\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\cap \left({j}+1\dots {M}+1\right)\right]=\varnothing$
194 185 193 sylan9req ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cap {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]=\varnothing$
195 simplr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1$
196 92 ad2antlr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to {2}^{nd}\left({k}\right)Fn\left(1\dots {M}+1\right)$
197 nn0p1nn ${⊢}{j}\in {ℕ}_{0}\to {j}+1\in ℕ$
198 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
199 197 198 eleqtrdi ${⊢}{j}\in {ℕ}_{0}\to {j}+1\in {ℤ}_{\ge 1}$
200 fzss1 ${⊢}{j}+1\in {ℤ}_{\ge 1}\to \left({j}+1\dots {M}+1\right)\subseteq \left(1\dots {M}+1\right)$
201 186 199 200 3syl ${⊢}{j}\in \left(0\dots {M}\right)\to \left({j}+1\dots {M}+1\right)\subseteq \left(1\dots {M}+1\right)$
202 elfzuz3 ${⊢}{j}\in \left(0\dots {M}\right)\to {M}\in {ℤ}_{\ge {j}}$
203 eluzp1p1 ${⊢}{M}\in {ℤ}_{\ge {j}}\to {M}+1\in {ℤ}_{\ge \left({j}+1\right)}$
204 eluzfz2 ${⊢}{M}+1\in {ℤ}_{\ge \left({j}+1\right)}\to {M}+1\in \left({j}+1\dots {M}+1\right)$
205 202 203 204 3syl ${⊢}{j}\in \left(0\dots {M}\right)\to {M}+1\in \left({j}+1\dots {M}+1\right)$
206 201 205 jca ${⊢}{j}\in \left(0\dots {M}\right)\to \left(\left({j}+1\dots {M}+1\right)\subseteq \left(1\dots {M}+1\right)\wedge {M}+1\in \left({j}+1\dots {M}+1\right)\right)$
207 fnfvima ${⊢}\left({2}^{nd}\left({k}\right)Fn\left(1\dots {M}+1\right)\wedge \left({j}+1\dots {M}+1\right)\subseteq \left(1\dots {M}+1\right)\wedge {M}+1\in \left({j}+1\dots {M}+1\right)\right)\to {2}^{nd}\left({k}\right)\left({M}+1\right)\in {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]$
208 207 3expb ${⊢}\left({2}^{nd}\left({k}\right)Fn\left(1\dots {M}+1\right)\wedge \left(\left({j}+1\dots {M}+1\right)\subseteq \left(1\dots {M}+1\right)\wedge {M}+1\in \left({j}+1\dots {M}+1\right)\right)\right)\to {2}^{nd}\left({k}\right)\left({M}+1\right)\in {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]$
209 196 206 208 syl2an ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {2}^{nd}\left({k}\right)\left({M}+1\right)\in {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]$
210 195 209 eqeltrrd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {M}+1\in {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]$
211 1ex ${⊢}1\in \mathrm{V}$
212 fnconstg ${⊢}1\in \mathrm{V}\to \left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]$
213 211 212 ax-mp ${⊢}\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]$
214 fnconstg ${⊢}0\in \mathrm{V}\to \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]$
215 166 214 ax-mp ${⊢}\left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]$
216 fvun2 ${⊢}\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\wedge \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]\wedge \left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cap {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]=\varnothing \wedge {M}+1\in {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]\right)\right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({M}+1\right)=\left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\left({M}+1\right)$
217 213 215 216 mp3an12 ${⊢}\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cap {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]=\varnothing \wedge {M}+1\in {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]\right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({M}+1\right)=\left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\left({M}+1\right)$
218 194 210 217 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({M}+1\right)=\left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\left({M}+1\right)$
219 166 fvconst2 ${⊢}{M}+1\in {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]\to \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\left({M}+1\right)=0$
220 210 219 syl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\left({M}+1\right)=0$
221 218 220 eqtrd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({M}+1\right)=0$
222 221 adantlrl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({M}+1\right)=0$
223 182 222 oveq12d ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {1}^{st}\left({k}\right)\left({M}+1\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({M}+1\right)=0+0$
224 00id ${⊢}0+0=0$
225 223 224 syl6eq ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {1}^{st}\left({k}\right)\left({M}+1\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({M}+1\right)=0$
226 181 225 sylan9eqr ${⊢}\left(\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {n}={M}+1\right)\to {1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)=0$
227 175 176 178 226 fmptapd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left\{⟨{M}+1,0⟩\right\}=\left({n}\in \left(1\dots {M}+1\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)$
228 227 uneq1d ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left\{⟨{M}+1,0⟩\right\}\right)\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)=\left({n}\in \left(1\dots {M}+1\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)$
229 174 228 eqtrd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left(\left({M}+1\dots {N}\right)×\left\{0\right\}\right)=\left({n}\in \left(1\dots {M}+1\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)$
230 elmapfn ${⊢}{1}^{st}\left({k}\right)\in \left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)\to {1}^{st}\left({k}\right)Fn\left(1\dots {M}+1\right)$
231 61 230 syl ${⊢}{k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\to {1}^{st}\left({k}\right)Fn\left(1\dots {M}+1\right)$
232 fnssres ${⊢}\left({1}^{st}\left({k}\right)Fn\left(1\dots {M}+1\right)\wedge \left(1\dots {M}\right)\subseteq \left(1\dots {M}+1\right)\right)\to \left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)Fn\left(1\dots {M}\right)$
233 231 64 232 sylancl ${⊢}{k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\to \left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)Fn\left(1\dots {M}\right)$
234 233 ad3antlr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)Fn\left(1\dots {M}\right)$
235 simplr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)$
236 fnconstg ${⊢}0\in \mathrm{V}\to \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]$
237 166 236 ax-mp ${⊢}\left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]$
238 213 237 pm3.2i ${⊢}\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\wedge \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]\right)$
239 imain ${⊢}\mathrm{Fun}{{2}^{nd}\left({k}\right)}^{-1}\to {2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\cap \left({j}+1\dots {M}\right)\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cap {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]$
240 76 83 239 3syl ${⊢}{k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\cap \left({j}+1\dots {M}\right)\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cap {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]$
241 fzdisj ${⊢}{j}<{j}+1\to \left(1\dots {j}\right)\cap \left({j}+1\dots {M}\right)=\varnothing$
242 188 241 syl ${⊢}{j}\in \left(0\dots {M}\right)\to \left(1\dots {j}\right)\cap \left({j}+1\dots {M}\right)=\varnothing$
243 242 imaeq2d ${⊢}{j}\in \left(0\dots {M}\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\cap \left({j}+1\dots {M}\right)\right]={2}^{nd}\left({k}\right)\left[\varnothing \right]$
244 243 192 syl6eq ${⊢}{j}\in \left(0\dots {M}\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\cap \left({j}+1\dots {M}\right)\right]=\varnothing$
245 240 244 sylan9req ${⊢}\left({k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cap {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]=\varnothing$
246 fnun ${⊢}\left(\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\wedge \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]\right)\wedge {2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cap {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]=\varnothing \right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)Fn\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cup {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]\right)$
247 238 245 246 sylancr ${⊢}\left({k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)Fn\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cup {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]\right)$
248 235 247 sylan ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)Fn\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cup {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]\right)$
249 101 adantr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\right]\setminus {2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]=\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}$
250 85 ad3antlr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\right]\setminus {2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]$
251 186 197 syl ${⊢}{j}\in \left(0\dots {M}\right)\to {j}+1\in ℕ$
252 251 198 eleqtrdi ${⊢}{j}\in \left(0\dots {M}\right)\to {j}+1\in {ℤ}_{\ge 1}$
253 fzsplit2 ${⊢}\left({j}+1\in {ℤ}_{\ge 1}\wedge {M}\in {ℤ}_{\ge {j}}\right)\to \left(1\dots {M}\right)=\left(1\dots {j}\right)\cup \left({j}+1\dots {M}\right)$
254 252 202 253 syl2anc ${⊢}{j}\in \left(0\dots {M}\right)\to \left(1\dots {M}\right)=\left(1\dots {j}\right)\cup \left({j}+1\dots {M}\right)$
255 128 254 sylan9eq ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}=\left(1\dots {j}\right)\cup \left({j}+1\dots {M}\right)$
256 255 imaeq2d ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\cup \left({j}+1\dots {M}\right)\right]$
257 250 256 eqtr3d ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\right]\setminus {2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\cup \left({j}+1\dots {M}\right)\right]$
258 125 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}=\left(1\dots {M}\right)$
259 249 257 258 3eqtr3rd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(1\dots {M}\right)={2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\cup \left({j}+1\dots {M}\right)\right]$
260 imaundi ${⊢}{2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\cup \left({j}+1\dots {M}\right)\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cup {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]$
261 259 260 syl6eq ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(1\dots {M}\right)={2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cup {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]$
262 261 fneq2d ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {M}\right)↔\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)Fn\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cup {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]\right)\right)$
263 248 262 mpbird ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {M}\right)$
264 fzss2 ${⊢}{M}\in {ℤ}_{\ge {j}}\to \left(1\dots {j}\right)\subseteq \left(1\dots {M}\right)$
265 resima2 ${⊢}\left(1\dots {j}\right)\subseteq \left(1\dots {M}\right)\to \left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left(1\dots {j}\right)\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]$
266 202 264 265 3syl ${⊢}{j}\in \left(0\dots {M}\right)\to \left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left(1\dots {j}\right)\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]$
267 266 xpeq1d ${⊢}{j}\in \left(0\dots {M}\right)\to \left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}={2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}$
268 186 199 syl ${⊢}{j}\in \left(0\dots {M}\right)\to {j}+1\in {ℤ}_{\ge 1}$
269 fzss1 ${⊢}{j}+1\in {ℤ}_{\ge 1}\to \left({j}+1\dots {M}\right)\subseteq \left(1\dots {M}\right)$
270 resima2 ${⊢}\left({j}+1\dots {M}\right)\subseteq \left(1\dots {M}\right)\to \left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left({j}+1\dots {M}\right)\right]={2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]$
271 268 269 270 3syl ${⊢}{j}\in \left(0\dots {M}\right)\to \left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left({j}+1\dots {M}\right)\right]={2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]$
272 271 xpeq1d ${⊢}{j}\in \left(0\dots {M}\right)\to \left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}={2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}$
273 267 272 uneq12d ${⊢}{j}\in \left(0\dots {M}\right)\to \left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)=\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)$
274 273 adantl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)=\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)$
275 274 fneq1d ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left(\left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {M}\right)↔\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {M}\right)\right)$
276 263 275 mpbird ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {M}\right)$
277 fzfid ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(1\dots {M}\right)\in \mathrm{Fin}$
278 inidm ${⊢}\left(1\dots {M}\right)\cap \left(1\dots {M}\right)=\left(1\dots {M}\right)$
279 fvres ${⊢}{n}\in \left(1\dots {M}\right)\to \left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left({n}\right)={1}^{st}\left({k}\right)\left({n}\right)$
280 279 adantl ${⊢}\left(\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {n}\in \left(1\dots {M}\right)\right)\to \left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left({n}\right)={1}^{st}\left({k}\right)\left({n}\right)$
281 disjsn ${⊢}\left(1\dots {M}\right)\cap \left\{{M}+1\right\}=\varnothing ↔¬{M}+1\in \left(1\dots {M}\right)$
282 122 281 sylibr ${⊢}{\phi }\to \left(1\dots {M}\right)\cap \left\{{M}+1\right\}=\varnothing$
283 282 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(1\dots {M}\right)\cap \left\{{M}+1\right\}=\varnothing$
284 263 283 jca ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {M}\right)\wedge \left(1\dots {M}\right)\cap \left\{{M}+1\right\}=\varnothing \right)$
285 fnconstg ${⊢}0\in \mathrm{V}\to \left(\left\{{M}+1\right\}×\left\{0\right\}\right)Fn\left\{{M}+1\right\}$
286 166 285 ax-mp ${⊢}\left(\left\{{M}+1\right\}×\left\{0\right\}\right)Fn\left\{{M}+1\right\}$
287 fvun1 ${⊢}\left(\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {M}\right)\wedge \left(\left\{{M}+1\right\}×\left\{0\right\}\right)Fn\left\{{M}+1\right\}\wedge \left(\left(1\dots {M}\right)\cap \left\{{M}+1\right\}=\varnothing \wedge {n}\in \left(1\dots {M}\right)\right)\right)\to \left(\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left(\left\{{M}+1\right\}×\left\{0\right\}\right)\right)\left({n}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)$
288 286 287 mp3an2 ${⊢}\left(\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {M}\right)\wedge \left(\left(1\dots {M}\right)\cap \left\{{M}+1\right\}=\varnothing \wedge {n}\in \left(1\dots {M}\right)\right)\right)\to \left(\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left(\left\{{M}+1\right\}×\left\{0\right\}\right)\right)\left({n}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)$
289 288 anassrs ${⊢}\left(\left(\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {M}\right)\wedge \left(1\dots {M}\right)\cap \left\{{M}+1\right\}=\varnothing \right)\wedge {n}\in \left(1\dots {M}\right)\right)\to \left(\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left(\left\{{M}+1\right\}×\left\{0\right\}\right)\right)\left({n}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)$
290 284 289 sylan ${⊢}\left(\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {n}\in \left(1\dots {M}\right)\right)\to \left(\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left(\left\{{M}+1\right\}×\left\{0\right\}\right)\right)\left({n}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)$
291 251 nnzd ${⊢}{j}\in \left(0\dots {M}\right)\to {j}+1\in ℤ$
292 186 nn0cnd ${⊢}{j}\in \left(0\dots {M}\right)\to {j}\in ℂ$
293 pncan1 ${⊢}{j}\in ℂ\to {j}+1-1={j}$
294 292 293 syl ${⊢}{j}\in \left(0\dots {M}\right)\to {j}+1-1={j}$
295 294 fveq2d ${⊢}{j}\in \left(0\dots {M}\right)\to {ℤ}_{\ge \left({j}+1-1\right)}={ℤ}_{\ge {j}}$
296 202 295 eleqtrrd ${⊢}{j}\in \left(0\dots {M}\right)\to {M}\in {ℤ}_{\ge \left({j}+1-1\right)}$
297 fzsuc2 ${⊢}\left({j}+1\in ℤ\wedge {M}\in {ℤ}_{\ge \left({j}+1-1\right)}\right)\to \left({j}+1\dots {M}+1\right)=\left({j}+1\dots {M}\right)\cup \left\{{M}+1\right\}$
298 291 296 297 syl2anc ${⊢}{j}\in \left(0\dots {M}\right)\to \left({j}+1\dots {M}+1\right)=\left({j}+1\dots {M}\right)\cup \left\{{M}+1\right\}$
299 298 imaeq2d ${⊢}{j}\in \left(0\dots {M}\right)\to {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]={2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\cup \left\{{M}+1\right\}\right]$
300 imaundi ${⊢}{2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\cup \left\{{M}+1\right\}\right]={2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]\cup {2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]$
301 299 300 syl6eq ${⊢}{j}\in \left(0\dots {M}\right)\to {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]={2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]\cup {2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]$
302 301 xpeq1d ${⊢}{j}\in \left(0\dots {M}\right)\to {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}=\left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]\cup {2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]\right)×\left\{0\right\}$
303 xpundir ${⊢}\left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]\cup {2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]\right)×\left\{0\right\}=\left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]×\left\{0\right\}\right)$
304 302 303 syl6eq ${⊢}{j}\in \left(0\dots {M}\right)\to {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}=\left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]×\left\{0\right\}\right)$
305 304 uneq2d ${⊢}{j}\in \left(0\dots {M}\right)\to \left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)=\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left(\left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]×\left\{0\right\}\right)\right)$
306 unass ${⊢}\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left({2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]×\left\{0\right\}\right)=\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left(\left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]×\left\{0\right\}\right)\right)$
307 305 306 syl6eqr ${⊢}{j}\in \left(0\dots {M}\right)\to \left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left({2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]×\left\{0\right\}\right)$
308 307 adantl ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left({2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]×\left\{0\right\}\right)$
309 98 xpeq1d ${⊢}\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\to \left\{{2}^{nd}\left({k}\right)\left({M}+1\right)\right\}×\left\{0\right\}={2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]×\left\{0\right\}$
310 309 uneq2d ${⊢}\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left(\left\{{2}^{nd}\left({k}\right)\left({M}+1\right)\right\}×\left\{0\right\}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left({2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]×\left\{0\right\}\right)$
311 310 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left(\left\{{2}^{nd}\left({k}\right)\left({M}+1\right)\right\}×\left\{0\right\}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left({2}^{nd}\left({k}\right)\left[\left\{{M}+1\right\}\right]×\left\{0\right\}\right)$
312 308 311 eqtr4d ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left(\left\{{2}^{nd}\left({k}\right)\left({M}+1\right)\right\}×\left\{0\right\}\right)$
313 99 xpeq1d ${⊢}{2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\to \left\{{2}^{nd}\left({k}\right)\left({M}+1\right)\right\}×\left\{0\right\}=\left\{{M}+1\right\}×\left\{0\right\}$
314 313 uneq2d ${⊢}{2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left(\left\{{2}^{nd}\left({k}\right)\left({M}+1\right)\right\}×\left\{0\right\}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left(\left\{{M}+1\right\}×\left\{0\right\}\right)$
315 312 314 sylan9eq ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to \left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left(\left\{{M}+1\right\}×\left\{0\right\}\right)$
316 315 an32s ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left(\left\{{M}+1\right\}×\left\{0\right\}\right)$
317 316 fveq1d ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)=\left(\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left(\left\{{M}+1\right\}×\left\{0\right\}\right)\right)\left({n}\right)$
318 317 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {n}\in \left(1\dots {M}\right)\right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)=\left(\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\cup \left(\left\{{M}+1\right\}×\left\{0\right\}\right)\right)\left({n}\right)$
319 273 fveq1d ${⊢}{j}\in \left(0\dots {M}\right)\to \left(\left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)$
320 319 ad2antlr ${⊢}\left(\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {n}\in \left(1\dots {M}\right)\right)\to \left(\left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)$
321 290 318 320 3eqtr4rd ${⊢}\left(\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {n}\in \left(1\dots {M}\right)\right)\to \left(\left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)$
322 234 276 277 277 278 280 321 offval ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right){+}_{f}\left(\left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)=\left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)$
323 322 uneq1d ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right){+}_{f}\left(\left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\right)\cup \left(\left({M}+1\dots {N}\right)×\left\{0\right\}\right)=\left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left(\left({M}+1\dots {N}\right)×\left\{0\right\}\right)$
324 323 adantlrl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right){+}_{f}\left(\left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\right)\cup \left(\left({M}+1\dots {N}\right)×\left\{0\right\}\right)=\left({n}\in \left(1\dots {M}\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left(\left({M}+1\dots {N}\right)×\left\{0\right\}\right)$
325 simplr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\to {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)$
326 231 adantr ${⊢}\left({k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {1}^{st}\left({k}\right)Fn\left(1\dots {M}+1\right)$
327 213 215 pm3.2i ${⊢}\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\wedge \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]\right)$
328 184 193 sylan9req ${⊢}\left({k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cap {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]=\varnothing$
329 fnun ${⊢}\left(\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\wedge \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]\right)\wedge {2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cap {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]=\varnothing \right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)Fn\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cup {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]\right)$
330 327 328 329 sylancr ${⊢}\left({k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)Fn\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cup {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]\right)$
331 peano2uz ${⊢}{M}\in {ℤ}_{\ge {j}}\to {M}+1\in {ℤ}_{\ge {j}}$
332 202 331 syl ${⊢}{j}\in \left(0\dots {M}\right)\to {M}+1\in {ℤ}_{\ge {j}}$
333 fzsplit2 ${⊢}\left({j}+1\in {ℤ}_{\ge 1}\wedge {M}+1\in {ℤ}_{\ge {j}}\right)\to \left(1\dots {M}+1\right)=\left(1\dots {j}\right)\cup \left({j}+1\dots {M}+1\right)$
334 268 332 333 syl2anc ${⊢}{j}\in \left(0\dots {M}\right)\to \left(1\dots {M}+1\right)=\left(1\dots {j}\right)\cup \left({j}+1\dots {M}+1\right)$
335 334 imaeq2d ${⊢}{j}\in \left(0\dots {M}\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\cup \left({j}+1\dots {M}+1\right)\right]$
336 imaundi ${⊢}{2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\cup \left({j}+1\dots {M}+1\right)\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cup {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]$
337 335 336 syl6req ${⊢}{j}\in \left(0\dots {M}\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cup {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]={2}^{nd}\left({k}\right)\left[\left(1\dots {M}+1\right)\right]$
338 337 89 sylan9eqr ${⊢}\left({k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cup {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]=\left(1\dots {M}+1\right)$
339 338 fneq2d ${⊢}\left({k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)Fn\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]\cup {2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]\right)↔\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {M}+1\right)\right)$
340 330 339 mpbid ${⊢}\left({k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {M}+1\right)$
341 fzfid ${⊢}\left({k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left(1\dots {M}+1\right)\in \mathrm{Fin}$
342 inidm ${⊢}\left(1\dots {M}+1\right)\cap \left(1\dots {M}+1\right)=\left(1\dots {M}+1\right)$
343 eqidd ${⊢}\left(\left({k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {n}\in \left(1\dots {M}+1\right)\right)\to {1}^{st}\left({k}\right)\left({n}\right)={1}^{st}\left({k}\right)\left({n}\right)$
344 eqidd ${⊢}\left(\left({k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {n}\in \left(1\dots {M}+1\right)\right)\to \left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)=\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)$
345 326 340 341 341 342 343 344 offval ${⊢}\left({k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to {1}^{st}\left({k}\right){+}_{f}\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)=\left({n}\in \left(1\dots {M}+1\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)$
346 345 uneq1d ${⊢}\left({k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({1}^{st}\left({k}\right){+}_{f}\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\right)\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)=\left({n}\in \left(1\dots {M}+1\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)$
347 325 346 sylan ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({1}^{st}\left({k}\right){+}_{f}\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\right)\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)=\left({n}\in \left(1\dots {M}+1\right)⟼{1}^{st}\left({k}\right)\left({n}\right)+\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\left({n}\right)\right)\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)$
348 229 324 347 3eqtr4rd ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({1}^{st}\left({k}\right){+}_{f}\left(\left({2}^{nd}\left({k}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({k}\right)\left[\left({j}+1\dots {M}+1\right)\right]×\left\{0\right\}\right)\right)\right)\cup \left(\left({M}+1+1\dots {N}\right)×\left\{0\right\}\right)=\left(\left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right){+}_{f}\left(\left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left(\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\left[\left({j}+1\dots {M}\right)\right]×\left\{0\right\}\right)\right)\right)\cup \left(\left({M}+1\dots {N}\right)×\left\{0\right\}\right)$
349 348 csbeq1d
350 349 eqeq2d
351 350 rexbidva
352 351 ralbidv
353 352 biimpd
354 353 impr
355 142 354 sylan2b
356 1st2nd2 ${⊢}{k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\to {k}=⟨{1}^{st}\left({k}\right),{2}^{nd}\left({k}\right)⟩$
357 356 ad2antlr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\to {k}=⟨{1}^{st}\left({k}\right),{2}^{nd}\left({k}\right)⟩$
358 fnsnsplit ${⊢}\left({1}^{st}\left({k}\right)Fn\left(1\dots {M}+1\right)\wedge {M}+1\in \left(1\dots {M}+1\right)\right)\to {1}^{st}\left({k}\right)=\left({{1}^{st}\left({k}\right)↾}_{\left(\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right)}\right)\cup \left\{⟨{M}+1,{1}^{st}\left({k}\right)\left({M}+1\right)⟩\right\}$
359 231 96 358 syl2anr ${⊢}\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\to {1}^{st}\left({k}\right)=\left({{1}^{st}\left({k}\right)↾}_{\left(\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right)}\right)\cup \left\{⟨{M}+1,{1}^{st}\left({k}\right)\left({M}+1\right)⟩\right\}$
360 359 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {1}^{st}\left({k}\right)\left({M}+1\right)=0\right)\to {1}^{st}\left({k}\right)=\left({{1}^{st}\left({k}\right)↾}_{\left(\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right)}\right)\cup \left\{⟨{M}+1,{1}^{st}\left({k}\right)\left({M}+1\right)⟩\right\}$
361 125 reseq2d ${⊢}{\phi }\to {{1}^{st}\left({k}\right)↾}_{\left(\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right)}={{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}$
362 361 adantr ${⊢}\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\to {{1}^{st}\left({k}\right)↾}_{\left(\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right)}={{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}$
363 opeq2 ${⊢}{1}^{st}\left({k}\right)\left({M}+1\right)=0\to ⟨{M}+1,{1}^{st}\left({k}\right)\left({M}+1\right)⟩=⟨{M}+1,0⟩$
364 363 sneqd ${⊢}{1}^{st}\left({k}\right)\left({M}+1\right)=0\to \left\{⟨{M}+1,{1}^{st}\left({k}\right)\left({M}+1\right)⟩\right\}=\left\{⟨{M}+1,0⟩\right\}$
365 uneq12 ${⊢}\left({{1}^{st}\left({k}\right)↾}_{\left(\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right)}={{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\wedge \left\{⟨{M}+1,{1}^{st}\left({k}\right)\left({M}+1\right)⟩\right\}=\left\{⟨{M}+1,0⟩\right\}\right)\to \left({{1}^{st}\left({k}\right)↾}_{\left(\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right)}\right)\cup \left\{⟨{M}+1,{1}^{st}\left({k}\right)\left({M}+1\right)⟩\right\}=\left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\cup \left\{⟨{M}+1,0⟩\right\}$
366 362 364 365 syl2an ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {1}^{st}\left({k}\right)\left({M}+1\right)=0\right)\to \left({{1}^{st}\left({k}\right)↾}_{\left(\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right)}\right)\cup \left\{⟨{M}+1,{1}^{st}\left({k}\right)\left({M}+1\right)⟩\right\}=\left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\cup \left\{⟨{M}+1,0⟩\right\}$
367 360 366 eqtrd ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {1}^{st}\left({k}\right)\left({M}+1\right)=0\right)\to {1}^{st}\left({k}\right)=\left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\cup \left\{⟨{M}+1,0⟩\right\}$
368 367 adantrr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\to {1}^{st}\left({k}\right)=\left({{1}^{st}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\cup \left\{⟨{M}+1,0⟩\right\}$
369 fnsnsplit ${⊢}\left({2}^{nd}\left({k}\right)Fn\left(1\dots {M}+1\right)\wedge {M}+1\in \left(1\dots {M}+1\right)\right)\to {2}^{nd}\left({k}\right)=\left({{2}^{nd}\left({k}\right)↾}_{\left(\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right)}\right)\cup \left\{⟨{M}+1,{2}^{nd}\left({k}\right)\left({M}+1\right)⟩\right\}$
370 92 96 369 syl2anr ${⊢}\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\to {2}^{nd}\left({k}\right)=\left({{2}^{nd}\left({k}\right)↾}_{\left(\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right)}\right)\cup \left\{⟨{M}+1,{2}^{nd}\left({k}\right)\left({M}+1\right)⟩\right\}$
371 370 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to {2}^{nd}\left({k}\right)=\left({{2}^{nd}\left({k}\right)↾}_{\left(\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right)}\right)\cup \left\{⟨{M}+1,{2}^{nd}\left({k}\right)\left({M}+1\right)⟩\right\}$
372 125 reseq2d ${⊢}{\phi }\to {{2}^{nd}\left({k}\right)↾}_{\left(\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right)}={{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}$
373 372 adantr ${⊢}\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\to {{2}^{nd}\left({k}\right)↾}_{\left(\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right)}={{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}$
374 opeq2 ${⊢}{2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\to ⟨{M}+1,{2}^{nd}\left({k}\right)\left({M}+1\right)⟩=⟨{M}+1,{M}+1⟩$
375 374 sneqd ${⊢}{2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\to \left\{⟨{M}+1,{2}^{nd}\left({k}\right)\left({M}+1\right)⟩\right\}=\left\{⟨{M}+1,{M}+1⟩\right\}$
376 uneq12 ${⊢}\left({{2}^{nd}\left({k}\right)↾}_{\left(\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right)}={{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\wedge \left\{⟨{M}+1,{2}^{nd}\left({k}\right)\left({M}+1\right)⟩\right\}=\left\{⟨{M}+1,{M}+1⟩\right\}\right)\to \left({{2}^{nd}\left({k}\right)↾}_{\left(\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right)}\right)\cup \left\{⟨{M}+1,{2}^{nd}\left({k}\right)\left({M}+1\right)⟩\right\}=\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}$
377 373 375 376 syl2an ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to \left({{2}^{nd}\left({k}\right)↾}_{\left(\left(1\dots {M}+1\right)\setminus \left\{{M}+1\right\}\right)}\right)\cup \left\{⟨{M}+1,{2}^{nd}\left({k}\right)\left({M}+1\right)⟩\right\}=\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}$
378 371 377 eqtrd ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\to {2}^{nd}\left({k}\right)=\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}$
379 378 adantrl ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}+1\right)=0\wedge {2}^{nd}\left({k}\right)\left({M}+1\right)={M}+1\right)\right)\to {2}^{nd}\left({k}\right)=\left({{2}^{nd}\left({k}\right)↾}_{\left(1\dots {M}\right)}\right)\cup \left\{⟨{M}+1,{M}+1⟩\right\}$
380 368 379 opeq12d ${⊢}\left(\left({\phi }\wedge {k}\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {M}+1\right)}\right)×\left\{{f}|{f}:\left(1\dots {M}+1\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+1\right)\right\}\right)\right)\wedge \left({1}^{st}\left({k}\right)\left({M}\right)\right)\right)$