# Metamath Proof Explorer

## Theorem poimirlem12

Description: Lemma for poimir connecting walks that could yield from a given cube a given face opposite the final vertex of the walk. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 ${⊢}{\phi }\to {N}\in ℕ$
poimirlem22.s
poimirlem22.1 ${⊢}{\phi }\to {F}:\left(0\dots {N}-1\right)⟶{\left(0\dots {K}\right)}^{\left(1\dots {N}\right)}$
poimirlem12.2 ${⊢}{\phi }\to {T}\in {S}$
poimirlem12.3 ${⊢}{\phi }\to {2}^{nd}\left({T}\right)={N}$
poimirlem12.4 ${⊢}{\phi }\to {U}\in {S}$
poimirlem12.5 ${⊢}{\phi }\to {2}^{nd}\left({U}\right)={N}$
poimirlem12.6 ${⊢}{\phi }\to {M}\in \left(0\dots {N}-1\right)$
Assertion poimirlem12 ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\subseteq {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]$

### Proof

Step Hyp Ref Expression
1 poimir.0 ${⊢}{\phi }\to {N}\in ℕ$
2 poimirlem22.s
3 poimirlem22.1 ${⊢}{\phi }\to {F}:\left(0\dots {N}-1\right)⟶{\left(0\dots {K}\right)}^{\left(1\dots {N}\right)}$
4 poimirlem12.2 ${⊢}{\phi }\to {T}\in {S}$
5 poimirlem12.3 ${⊢}{\phi }\to {2}^{nd}\left({T}\right)={N}$
6 poimirlem12.4 ${⊢}{\phi }\to {U}\in {S}$
7 poimirlem12.5 ${⊢}{\phi }\to {2}^{nd}\left({U}\right)={N}$
8 poimirlem12.6 ${⊢}{\phi }\to {M}\in \left(0\dots {N}-1\right)$
9 eldif ${⊢}{y}\in \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\right)↔\left({y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\wedge ¬{y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\right)$
10 imassrn ${⊢}{2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\subseteq \mathrm{ran}{2}^{nd}\left({1}^{st}\left({T}\right)\right)$
11 elrabi
12 11 2 eleq2s ${⊢}{T}\in {S}\to {T}\in \left(\left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)×\left(0\dots {N}\right)\right)$
13 xp1st ${⊢}{T}\in \left(\left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)×\left(0\dots {N}\right)\right)\to {1}^{st}\left({T}\right)\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)$
14 4 12 13 3syl ${⊢}{\phi }\to {1}^{st}\left({T}\right)\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)$
15 xp2nd ${⊢}{1}^{st}\left({T}\right)\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\in \left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}$
16 14 15 syl ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\in \left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}$
17 fvex ${⊢}{2}^{nd}\left({1}^{st}\left({T}\right)\right)\in \mathrm{V}$
18 f1oeq1 ${⊢}{f}={2}^{nd}\left({1}^{st}\left({T}\right)\right)\to \left({f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)↔{2}^{nd}\left({1}^{st}\left({T}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right)$
19 17 18 elab ${⊢}{2}^{nd}\left({1}^{st}\left({T}\right)\right)\in \left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}↔{2}^{nd}\left({1}^{st}\left({T}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)$
20 16 19 sylib ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({T}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)$
21 f1of ${⊢}{2}^{nd}\left({1}^{st}\left({T}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\to {2}^{nd}\left({1}^{st}\left({T}\right)\right):\left(1\dots {N}\right)⟶\left(1\dots {N}\right)$
22 frn ${⊢}{2}^{nd}\left({1}^{st}\left({T}\right)\right):\left(1\dots {N}\right)⟶\left(1\dots {N}\right)\to \mathrm{ran}{2}^{nd}\left({1}^{st}\left({T}\right)\right)\subseteq \left(1\dots {N}\right)$
23 20 21 22 3syl ${⊢}{\phi }\to \mathrm{ran}{2}^{nd}\left({1}^{st}\left({T}\right)\right)\subseteq \left(1\dots {N}\right)$
24 10 23 sstrid ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\subseteq \left(1\dots {N}\right)$
25 elrabi
26 25 2 eleq2s ${⊢}{U}\in {S}\to {U}\in \left(\left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)×\left(0\dots {N}\right)\right)$
27 xp1st ${⊢}{U}\in \left(\left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)×\left(0\dots {N}\right)\right)\to {1}^{st}\left({U}\right)\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)$
28 6 26 27 3syl ${⊢}{\phi }\to {1}^{st}\left({U}\right)\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)$
29 xp2nd ${⊢}{1}^{st}\left({U}\right)\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\in \left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}$
30 28 29 syl ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\in \left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}$
31 fvex ${⊢}{2}^{nd}\left({1}^{st}\left({U}\right)\right)\in \mathrm{V}$
32 f1oeq1 ${⊢}{f}={2}^{nd}\left({1}^{st}\left({U}\right)\right)\to \left({f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)↔{2}^{nd}\left({1}^{st}\left({U}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right)$
33 31 32 elab ${⊢}{2}^{nd}\left({1}^{st}\left({U}\right)\right)\in \left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}↔{2}^{nd}\left({1}^{st}\left({U}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)$
34 30 33 sylib ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({U}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)$
35 f1ofo ${⊢}{2}^{nd}\left({1}^{st}\left({U}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\to {2}^{nd}\left({1}^{st}\left({U}\right)\right):\left(1\dots {N}\right)\underset{onto}{⟶}\left(1\dots {N}\right)$
36 foima ${⊢}{2}^{nd}\left({1}^{st}\left({U}\right)\right):\left(1\dots {N}\right)\underset{onto}{⟶}\left(1\dots {N}\right)\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {N}\right)\right]=\left(1\dots {N}\right)$
37 34 35 36 3syl ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {N}\right)\right]=\left(1\dots {N}\right)$
38 24 37 sseqtrrd ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\subseteq {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {N}\right)\right]$
39 38 ssdifd ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\subseteq {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {N}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]$
40 dff1o3 ${⊢}{2}^{nd}\left({1}^{st}\left({U}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)↔\left({2}^{nd}\left({1}^{st}\left({U}\right)\right):\left(1\dots {N}\right)\underset{onto}{⟶}\left(1\dots {N}\right)\wedge \mathrm{Fun}{{2}^{nd}\left({1}^{st}\left({U}\right)\right)}^{-1}\right)$
41 40 simprbi ${⊢}{2}^{nd}\left({1}^{st}\left({U}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\to \mathrm{Fun}{{2}^{nd}\left({1}^{st}\left({U}\right)\right)}^{-1}$
42 imadif ${⊢}\mathrm{Fun}{{2}^{nd}\left({1}^{st}\left({U}\right)\right)}^{-1}\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {N}\right)\setminus \left(1\dots {M}\right)\right]={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {N}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]$
43 34 41 42 3syl ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {N}\right)\setminus \left(1\dots {M}\right)\right]={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {N}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]$
44 difun2 ${⊢}\left(\left({M}+1\dots {N}\right)\cup \left(1\dots {M}\right)\right)\setminus \left(1\dots {M}\right)=\left({M}+1\dots {N}\right)\setminus \left(1\dots {M}\right)$
45 elfznn0 ${⊢}{M}\in \left(0\dots {N}-1\right)\to {M}\in {ℕ}_{0}$
46 nn0p1nn ${⊢}{M}\in {ℕ}_{0}\to {M}+1\in ℕ$
47 8 45 46 3syl ${⊢}{\phi }\to {M}+1\in ℕ$
48 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
49 47 48 eleqtrdi ${⊢}{\phi }\to {M}+1\in {ℤ}_{\ge 1}$
50 1 nncnd ${⊢}{\phi }\to {N}\in ℂ$
51 npcan1 ${⊢}{N}\in ℂ\to {N}-1+1={N}$
52 50 51 syl ${⊢}{\phi }\to {N}-1+1={N}$
53 elfzuz3 ${⊢}{M}\in \left(0\dots {N}-1\right)\to {N}-1\in {ℤ}_{\ge {M}}$
54 peano2uz ${⊢}{N}-1\in {ℤ}_{\ge {M}}\to {N}-1+1\in {ℤ}_{\ge {M}}$
55 8 53 54 3syl ${⊢}{\phi }\to {N}-1+1\in {ℤ}_{\ge {M}}$
56 52 55 eqeltrrd ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
57 fzsplit2 ${⊢}\left({M}+1\in {ℤ}_{\ge 1}\wedge {N}\in {ℤ}_{\ge {M}}\right)\to \left(1\dots {N}\right)=\left(1\dots {M}\right)\cup \left({M}+1\dots {N}\right)$
58 49 56 57 syl2anc ${⊢}{\phi }\to \left(1\dots {N}\right)=\left(1\dots {M}\right)\cup \left({M}+1\dots {N}\right)$
59 uncom ${⊢}\left(1\dots {M}\right)\cup \left({M}+1\dots {N}\right)=\left({M}+1\dots {N}\right)\cup \left(1\dots {M}\right)$
60 58 59 syl6eq ${⊢}{\phi }\to \left(1\dots {N}\right)=\left({M}+1\dots {N}\right)\cup \left(1\dots {M}\right)$
61 60 difeq1d ${⊢}{\phi }\to \left(1\dots {N}\right)\setminus \left(1\dots {M}\right)=\left(\left({M}+1\dots {N}\right)\cup \left(1\dots {M}\right)\right)\setminus \left(1\dots {M}\right)$
62 incom ${⊢}\left({M}+1\dots {N}\right)\cap \left(1\dots {M}\right)=\left(1\dots {M}\right)\cap \left({M}+1\dots {N}\right)$
63 8 45 syl ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
64 63 nn0red ${⊢}{\phi }\to {M}\in ℝ$
65 64 ltp1d ${⊢}{\phi }\to {M}<{M}+1$
66 fzdisj ${⊢}{M}<{M}+1\to \left(1\dots {M}\right)\cap \left({M}+1\dots {N}\right)=\varnothing$
67 65 66 syl ${⊢}{\phi }\to \left(1\dots {M}\right)\cap \left({M}+1\dots {N}\right)=\varnothing$
68 62 67 syl5eq ${⊢}{\phi }\to \left({M}+1\dots {N}\right)\cap \left(1\dots {M}\right)=\varnothing$
69 disj3 ${⊢}\left({M}+1\dots {N}\right)\cap \left(1\dots {M}\right)=\varnothing ↔\left({M}+1\dots {N}\right)=\left({M}+1\dots {N}\right)\setminus \left(1\dots {M}\right)$
70 68 69 sylib ${⊢}{\phi }\to \left({M}+1\dots {N}\right)=\left({M}+1\dots {N}\right)\setminus \left(1\dots {M}\right)$
71 44 61 70 3eqtr4a ${⊢}{\phi }\to \left(1\dots {N}\right)\setminus \left(1\dots {M}\right)=\left({M}+1\dots {N}\right)$
72 71 imaeq2d ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {N}\right)\setminus \left(1\dots {M}\right)\right]={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
73 43 72 eqtr3d ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {N}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
74 39 73 sseqtrd ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\subseteq {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
75 74 sselda ${⊢}\left({\phi }\wedge {y}\in \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\right)\to {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
76 9 75 sylan2br ${⊢}\left({\phi }\wedge \left({y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\wedge ¬{y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\right)\to {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
77 fveq2 ${⊢}{t}={U}\to {2}^{nd}\left({t}\right)={2}^{nd}\left({U}\right)$
78 77 breq2d ${⊢}{t}={U}\to \left({y}<{2}^{nd}\left({t}\right)↔{y}<{2}^{nd}\left({U}\right)\right)$
79 78 ifbid ${⊢}{t}={U}\to if\left({y}<{2}^{nd}\left({t}\right),{y},{y}+1\right)=if\left({y}<{2}^{nd}\left({U}\right),{y},{y}+1\right)$
80 79 csbeq1d
81 2fveq3 ${⊢}{t}={U}\to {1}^{st}\left({1}^{st}\left({t}\right)\right)={1}^{st}\left({1}^{st}\left({U}\right)\right)$
82 2fveq3 ${⊢}{t}={U}\to {2}^{nd}\left({1}^{st}\left({t}\right)\right)={2}^{nd}\left({1}^{st}\left({U}\right)\right)$
83 82 imaeq1d ${⊢}{t}={U}\to {2}^{nd}\left({1}^{st}\left({t}\right)\right)\left[\left(1\dots {j}\right)\right]={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {j}\right)\right]$
84 83 xpeq1d ${⊢}{t}={U}\to {2}^{nd}\left({1}^{st}\left({t}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}$
85 82 imaeq1d ${⊢}{t}={U}\to {2}^{nd}\left({1}^{st}\left({t}\right)\right)\left[\left({j}+1\dots {N}\right)\right]={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({j}+1\dots {N}\right)\right]$
86 85 xpeq1d ${⊢}{t}={U}\to {2}^{nd}\left({1}^{st}\left({t}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}$
87 84 86 uneq12d ${⊢}{t}={U}\to \left({2}^{nd}\left({1}^{st}\left({t}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({t}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}\right)=\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}\right)$
88 81 87 oveq12d ${⊢}{t}={U}\to {1}^{st}\left({1}^{st}\left({t}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({t}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({t}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)={1}^{st}\left({1}^{st}\left({U}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)$
89 88 csbeq2dv
90 80 89 eqtrd
91 90 mpteq2dv
92 91 eqeq2d
93 92 2 elrab2
94 93 simprbi
95 6 94 syl
96 breq1 ${⊢}{y}={M}\to \left({y}<{2}^{nd}\left({U}\right)↔{M}<{2}^{nd}\left({U}\right)\right)$
97 id ${⊢}{y}={M}\to {y}={M}$
98 96 97 ifbieq1d ${⊢}{y}={M}\to if\left({y}<{2}^{nd}\left({U}\right),{y},{y}+1\right)=if\left({M}<{2}^{nd}\left({U}\right),{M},{y}+1\right)$
99 1 nnred ${⊢}{\phi }\to {N}\in ℝ$
100 peano2rem ${⊢}{N}\in ℝ\to {N}-1\in ℝ$
101 99 100 syl ${⊢}{\phi }\to {N}-1\in ℝ$
102 elfzle2 ${⊢}{M}\in \left(0\dots {N}-1\right)\to {M}\le {N}-1$
103 8 102 syl ${⊢}{\phi }\to {M}\le {N}-1$
104 99 ltm1d ${⊢}{\phi }\to {N}-1<{N}$
105 64 101 99 103 104 lelttrd ${⊢}{\phi }\to {M}<{N}$
106 105 7 breqtrrd ${⊢}{\phi }\to {M}<{2}^{nd}\left({U}\right)$
107 106 iftrued ${⊢}{\phi }\to if\left({M}<{2}^{nd}\left({U}\right),{M},{y}+1\right)={M}$
108 98 107 sylan9eqr ${⊢}\left({\phi }\wedge {y}={M}\right)\to if\left({y}<{2}^{nd}\left({U}\right),{y},{y}+1\right)={M}$
109 108 csbeq1d
110 oveq2 ${⊢}{j}={M}\to \left(1\dots {j}\right)=\left(1\dots {M}\right)$
111 110 imaeq2d ${⊢}{j}={M}\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {j}\right)\right]={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]$
112 111 xpeq1d ${⊢}{j}={M}\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}$
113 oveq1 ${⊢}{j}={M}\to {j}+1={M}+1$
114 113 oveq1d ${⊢}{j}={M}\to \left({j}+1\dots {N}\right)=\left({M}+1\dots {N}\right)$
115 114 imaeq2d ${⊢}{j}={M}\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({j}+1\dots {N}\right)\right]={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
116 115 xpeq1d ${⊢}{j}={M}\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}$
117 112 116 uneq12d ${⊢}{j}={M}\to \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}\right)=\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)$
118 117 oveq2d ${⊢}{j}={M}\to {1}^{st}\left({1}^{st}\left({U}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)={1}^{st}\left({1}^{st}\left({U}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)$
119 118 adantl ${⊢}\left({\phi }\wedge {j}={M}\right)\to {1}^{st}\left({1}^{st}\left({U}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)={1}^{st}\left({1}^{st}\left({U}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)$
120 8 119 csbied
122 109 121 eqtrd
123 ovexd ${⊢}{\phi }\to {1}^{st}\left({1}^{st}\left({U}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\in \mathrm{V}$
124 95 122 8 123 fvmptd ${⊢}{\phi }\to {F}\left({M}\right)={1}^{st}\left({1}^{st}\left({U}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)$
125 124 fveq1d ${⊢}{\phi }\to {F}\left({M}\right)\left({y}\right)=\left({1}^{st}\left({1}^{st}\left({U}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\right)\left({y}\right)$
126 125 adantr ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\to {F}\left({M}\right)\left({y}\right)=\left({1}^{st}\left({1}^{st}\left({U}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\right)\left({y}\right)$
127 imassrn ${⊢}{2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\subseteq \mathrm{ran}{2}^{nd}\left({1}^{st}\left({U}\right)\right)$
128 f1of ${⊢}{2}^{nd}\left({1}^{st}\left({U}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\to {2}^{nd}\left({1}^{st}\left({U}\right)\right):\left(1\dots {N}\right)⟶\left(1\dots {N}\right)$
129 frn ${⊢}{2}^{nd}\left({1}^{st}\left({U}\right)\right):\left(1\dots {N}\right)⟶\left(1\dots {N}\right)\to \mathrm{ran}{2}^{nd}\left({1}^{st}\left({U}\right)\right)\subseteq \left(1\dots {N}\right)$
130 34 128 129 3syl ${⊢}{\phi }\to \mathrm{ran}{2}^{nd}\left({1}^{st}\left({U}\right)\right)\subseteq \left(1\dots {N}\right)$
131 127 130 sstrid ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\subseteq \left(1\dots {N}\right)$
132 131 sselda ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\to {y}\in \left(1\dots {N}\right)$
133 xp1st ${⊢}{1}^{st}\left({U}\right)\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)\to {1}^{st}\left({1}^{st}\left({U}\right)\right)\in \left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)$
134 elmapfn ${⊢}{1}^{st}\left({1}^{st}\left({U}\right)\right)\in \left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)\to {1}^{st}\left({1}^{st}\left({U}\right)\right)Fn\left(1\dots {N}\right)$
135 28 133 134 3syl ${⊢}{\phi }\to {1}^{st}\left({1}^{st}\left({U}\right)\right)Fn\left(1\dots {N}\right)$
136 135 adantr ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\to {1}^{st}\left({1}^{st}\left({U}\right)\right)Fn\left(1\dots {N}\right)$
137 1ex ${⊢}1\in \mathrm{V}$
138 fnconstg ${⊢}1\in \mathrm{V}\to \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]$
139 137 138 ax-mp ${⊢}\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]$
140 c0ex ${⊢}0\in \mathrm{V}$
141 fnconstg ${⊢}0\in \mathrm{V}\to \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
142 140 141 ax-mp ${⊢}\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
143 139 142 pm3.2i ${⊢}\left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\wedge \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)$
144 imain ${⊢}\mathrm{Fun}{{2}^{nd}\left({1}^{st}\left({U}\right)\right)}^{-1}\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\cap \left({M}+1\dots {N}\right)\right]={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\cap {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
145 34 41 144 3syl ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\cap \left({M}+1\dots {N}\right)\right]={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\cap {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
146 67 imaeq2d ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\cap \left({M}+1\dots {N}\right)\right]={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\varnothing \right]$
147 ima0 ${⊢}{2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\varnothing \right]=\varnothing$
148 146 147 syl6eq ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\cap \left({M}+1\dots {N}\right)\right]=\varnothing$
149 145 148 eqtr3d ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\cap {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]=\varnothing$
150 fnun ${⊢}\left(\left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\wedge \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\wedge {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\cap {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]=\varnothing \right)\to \left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)Fn\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\cup {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)$
151 143 149 150 sylancr ${⊢}{\phi }\to \left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)Fn\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\cup {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)$
152 imaundi ${⊢}{2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\cup \left({M}+1\dots {N}\right)\right]={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\cup {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
153 58 imaeq2d ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {N}\right)\right]={2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\cup \left({M}+1\dots {N}\right)\right]$
154 153 37 eqtr3d ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\cup \left({M}+1\dots {N}\right)\right]=\left(1\dots {N}\right)$
155 152 154 syl5eqr ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\cup {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]=\left(1\dots {N}\right)$
156 155 fneq2d ${⊢}{\phi }\to \left(\left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)Fn\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\cup {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)↔\left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {N}\right)\right)$
157 151 156 mpbid ${⊢}{\phi }\to \left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {N}\right)$
158 157 adantr ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\to \left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {N}\right)$
159 ovexd ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\to \left(1\dots {N}\right)\in \mathrm{V}$
160 inidm ${⊢}\left(1\dots {N}\right)\cap \left(1\dots {N}\right)=\left(1\dots {N}\right)$
161 eqidd ${⊢}\left(\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\wedge {y}\in \left(1\dots {N}\right)\right)\to {1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)={1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)$
162 fvun2 ${⊢}\left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\wedge \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\wedge \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\cap {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]=\varnothing \wedge {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\right)\to \left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\left({y}\right)=\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\left({y}\right)$
163 139 142 162 mp3an12 ${⊢}\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\cap {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]=\varnothing \wedge {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\to \left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\left({y}\right)=\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\left({y}\right)$
164 149 163 sylan ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\to \left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\left({y}\right)=\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\left({y}\right)$
165 140 fvconst2 ${⊢}{y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\to \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\left({y}\right)=0$
166 165 adantl ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\to \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\left({y}\right)=0$
167 164 166 eqtrd ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\to \left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\left({y}\right)=0$
168 167 adantr ${⊢}\left(\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\wedge {y}\in \left(1\dots {N}\right)\right)\to \left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\left({y}\right)=0$
169 136 158 159 159 160 161 168 ofval ${⊢}\left(\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\wedge {y}\in \left(1\dots {N}\right)\right)\to \left({1}^{st}\left({1}^{st}\left({U}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\right)\left({y}\right)={1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)+0$
170 132 169 mpdan ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\to \left({1}^{st}\left({1}^{st}\left({U}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\right)\left({y}\right)={1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)+0$
171 elmapi ${⊢}{1}^{st}\left({1}^{st}\left({U}\right)\right)\in \left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)\to {1}^{st}\left({1}^{st}\left({U}\right)\right):\left(1\dots {N}\right)⟶\left(0..^{K}\right)$
172 28 133 171 3syl ${⊢}{\phi }\to {1}^{st}\left({1}^{st}\left({U}\right)\right):\left(1\dots {N}\right)⟶\left(0..^{K}\right)$
173 172 ffvelrnda ${⊢}\left({\phi }\wedge {y}\in \left(1\dots {N}\right)\right)\to {1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)\in \left(0..^{K}\right)$
174 elfzonn0 ${⊢}{1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)\in \left(0..^{K}\right)\to {1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)\in {ℕ}_{0}$
175 173 174 syl ${⊢}\left({\phi }\wedge {y}\in \left(1\dots {N}\right)\right)\to {1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)\in {ℕ}_{0}$
176 175 nn0cnd ${⊢}\left({\phi }\wedge {y}\in \left(1\dots {N}\right)\right)\to {1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)\in ℂ$
177 176 addid1d ${⊢}\left({\phi }\wedge {y}\in \left(1\dots {N}\right)\right)\to {1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)+0={1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)$
178 132 177 syldan ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\to {1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)+0={1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)$
179 126 170 178 3eqtrd ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\to {F}\left({M}\right)\left({y}\right)={1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)$
180 76 179 syldan ${⊢}\left({\phi }\wedge \left({y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\wedge ¬{y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\right)\to {F}\left({M}\right)\left({y}\right)={1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)$
181 fveq2 ${⊢}{t}={T}\to {2}^{nd}\left({t}\right)={2}^{nd}\left({T}\right)$
182 181 breq2d ${⊢}{t}={T}\to \left({y}<{2}^{nd}\left({t}\right)↔{y}<{2}^{nd}\left({T}\right)\right)$
183 182 ifbid ${⊢}{t}={T}\to if\left({y}<{2}^{nd}\left({t}\right),{y},{y}+1\right)=if\left({y}<{2}^{nd}\left({T}\right),{y},{y}+1\right)$
184 183 csbeq1d
185 2fveq3 ${⊢}{t}={T}\to {1}^{st}\left({1}^{st}\left({t}\right)\right)={1}^{st}\left({1}^{st}\left({T}\right)\right)$
186 2fveq3 ${⊢}{t}={T}\to {2}^{nd}\left({1}^{st}\left({t}\right)\right)={2}^{nd}\left({1}^{st}\left({T}\right)\right)$
187 186 imaeq1d ${⊢}{t}={T}\to {2}^{nd}\left({1}^{st}\left({t}\right)\right)\left[\left(1\dots {j}\right)\right]={2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {j}\right)\right]$
188 187 xpeq1d ${⊢}{t}={T}\to {2}^{nd}\left({1}^{st}\left({t}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}={2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}$
189 186 imaeq1d ${⊢}{t}={T}\to {2}^{nd}\left({1}^{st}\left({t}\right)\right)\left[\left({j}+1\dots {N}\right)\right]={2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({j}+1\dots {N}\right)\right]$
190 189 xpeq1d ${⊢}{t}={T}\to {2}^{nd}\left({1}^{st}\left({t}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}={2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}$
191 188 190 uneq12d ${⊢}{t}={T}\to \left({2}^{nd}\left({1}^{st}\left({t}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({t}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}\right)=\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}\right)$
192 185 191 oveq12d ${⊢}{t}={T}\to {1}^{st}\left({1}^{st}\left({t}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({t}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({t}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)={1}^{st}\left({1}^{st}\left({T}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)$
193 192 csbeq2dv
194 184 193 eqtrd
195 194 mpteq2dv
196 195 eqeq2d
197 196 2 elrab2
198 197 simprbi
199 4 198 syl
200 breq1 ${⊢}{y}={M}\to \left({y}<{2}^{nd}\left({T}\right)↔{M}<{2}^{nd}\left({T}\right)\right)$
201 200 97 ifbieq1d ${⊢}{y}={M}\to if\left({y}<{2}^{nd}\left({T}\right),{y},{y}+1\right)=if\left({M}<{2}^{nd}\left({T}\right),{M},{y}+1\right)$
202 105 5 breqtrrd ${⊢}{\phi }\to {M}<{2}^{nd}\left({T}\right)$
203 202 iftrued ${⊢}{\phi }\to if\left({M}<{2}^{nd}\left({T}\right),{M},{y}+1\right)={M}$
204 201 203 sylan9eqr ${⊢}\left({\phi }\wedge {y}={M}\right)\to if\left({y}<{2}^{nd}\left({T}\right),{y},{y}+1\right)={M}$
205 204 csbeq1d
206 110 imaeq2d ${⊢}{j}={M}\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {j}\right)\right]={2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]$
207 206 xpeq1d ${⊢}{j}={M}\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}={2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}$
208 114 imaeq2d ${⊢}{j}={M}\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({j}+1\dots {N}\right)\right]={2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
209 208 xpeq1d ${⊢}{j}={M}\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}={2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}$
210 207 209 uneq12d ${⊢}{j}={M}\to \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}\right)=\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)$
211 210 oveq2d ${⊢}{j}={M}\to {1}^{st}\left({1}^{st}\left({T}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)={1}^{st}\left({1}^{st}\left({T}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)$
212 211 adantl ${⊢}\left({\phi }\wedge {j}={M}\right)\to {1}^{st}\left({1}^{st}\left({T}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {j}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({j}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)={1}^{st}\left({1}^{st}\left({T}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)$
213 8 212 csbied
215 205 214 eqtrd
216 ovexd ${⊢}{\phi }\to {1}^{st}\left({1}^{st}\left({T}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\in \mathrm{V}$
217 199 215 8 216 fvmptd ${⊢}{\phi }\to {F}\left({M}\right)={1}^{st}\left({1}^{st}\left({T}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)$
218 217 fveq1d ${⊢}{\phi }\to {F}\left({M}\right)\left({y}\right)=\left({1}^{st}\left({1}^{st}\left({T}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\right)\left({y}\right)$
219 218 adantr ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\to {F}\left({M}\right)\left({y}\right)=\left({1}^{st}\left({1}^{st}\left({T}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\right)\left({y}\right)$
220 24 sselda ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\to {y}\in \left(1\dots {N}\right)$
221 xp1st ${⊢}{1}^{st}\left({T}\right)\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)\to {1}^{st}\left({1}^{st}\left({T}\right)\right)\in \left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)$
222 elmapfn ${⊢}{1}^{st}\left({1}^{st}\left({T}\right)\right)\in \left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)\to {1}^{st}\left({1}^{st}\left({T}\right)\right)Fn\left(1\dots {N}\right)$
223 14 221 222 3syl ${⊢}{\phi }\to {1}^{st}\left({1}^{st}\left({T}\right)\right)Fn\left(1\dots {N}\right)$
224 223 adantr ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\to {1}^{st}\left({1}^{st}\left({T}\right)\right)Fn\left(1\dots {N}\right)$
225 fnconstg ${⊢}1\in \mathrm{V}\to \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]$
226 137 225 ax-mp ${⊢}\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]$
227 fnconstg ${⊢}0\in \mathrm{V}\to \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
228 140 227 ax-mp ${⊢}\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
229 226 228 pm3.2i ${⊢}\left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\wedge \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)$
230 dff1o3 ${⊢}{2}^{nd}\left({1}^{st}\left({T}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)↔\left({2}^{nd}\left({1}^{st}\left({T}\right)\right):\left(1\dots {N}\right)\underset{onto}{⟶}\left(1\dots {N}\right)\wedge \mathrm{Fun}{{2}^{nd}\left({1}^{st}\left({T}\right)\right)}^{-1}\right)$
231 230 simprbi ${⊢}{2}^{nd}\left({1}^{st}\left({T}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\to \mathrm{Fun}{{2}^{nd}\left({1}^{st}\left({T}\right)\right)}^{-1}$
232 imain ${⊢}\mathrm{Fun}{{2}^{nd}\left({1}^{st}\left({T}\right)\right)}^{-1}\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\cap \left({M}+1\dots {N}\right)\right]={2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\cap {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
233 20 231 232 3syl ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\cap \left({M}+1\dots {N}\right)\right]={2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\cap {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
234 67 imaeq2d ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\cap \left({M}+1\dots {N}\right)\right]={2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\varnothing \right]$
235 ima0 ${⊢}{2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\varnothing \right]=\varnothing$
236 234 235 syl6eq ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\cap \left({M}+1\dots {N}\right)\right]=\varnothing$
237 233 236 eqtr3d ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\cap {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]=\varnothing$
238 fnun ${⊢}\left(\left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\wedge \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)\wedge {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\cap {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]=\varnothing \right)\to \left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)Fn\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\cup {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)$
239 229 237 238 sylancr ${⊢}{\phi }\to \left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)Fn\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\cup {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)$
240 imaundi ${⊢}{2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\cup \left({M}+1\dots {N}\right)\right]={2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\cup {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]$
241 58 imaeq2d ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {N}\right)\right]={2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\cup \left({M}+1\dots {N}\right)\right]$
242 f1ofo ${⊢}{2}^{nd}\left({1}^{st}\left({T}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\to {2}^{nd}\left({1}^{st}\left({T}\right)\right):\left(1\dots {N}\right)\underset{onto}{⟶}\left(1\dots {N}\right)$
243 foima ${⊢}{2}^{nd}\left({1}^{st}\left({T}\right)\right):\left(1\dots {N}\right)\underset{onto}{⟶}\left(1\dots {N}\right)\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {N}\right)\right]=\left(1\dots {N}\right)$
244 20 242 243 3syl ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {N}\right)\right]=\left(1\dots {N}\right)$
245 241 244 eqtr3d ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\cup \left({M}+1\dots {N}\right)\right]=\left(1\dots {N}\right)$
246 240 245 syl5eqr ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\cup {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]=\left(1\dots {N}\right)$
247 246 fneq2d ${⊢}{\phi }\to \left(\left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)Fn\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\cup {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\right)↔\left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {N}\right)\right)$
248 239 247 mpbid ${⊢}{\phi }\to \left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {N}\right)$
249 248 adantr ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\to \left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)Fn\left(1\dots {N}\right)$
250 ovexd ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\to \left(1\dots {N}\right)\in \mathrm{V}$
251 eqidd ${⊢}\left(\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\wedge {y}\in \left(1\dots {N}\right)\right)\to {1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)={1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)$
252 fvun1 ${⊢}\left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\wedge \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)Fn{2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]\wedge \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\cap {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]=\varnothing \wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\right)\to \left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\left({y}\right)=\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\left({y}\right)$
253 226 228 252 mp3an12 ${⊢}\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\cap {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]=\varnothing \wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\to \left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\left({y}\right)=\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\left({y}\right)$
254 237 253 sylan ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\to \left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\left({y}\right)=\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\left({y}\right)$
255 137 fvconst2 ${⊢}{y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\to \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\left({y}\right)=1$
256 255 adantl ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\to \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\left({y}\right)=1$
257 254 256 eqtrd ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\to \left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\left({y}\right)=1$
258 257 adantr ${⊢}\left(\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\wedge {y}\in \left(1\dots {N}\right)\right)\to \left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\left({y}\right)=1$
259 224 249 250 250 160 251 258 ofval ${⊢}\left(\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\wedge {y}\in \left(1\dots {N}\right)\right)\to \left({1}^{st}\left({1}^{st}\left({T}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\right)\left({y}\right)={1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)+1$
260 220 259 mpdan ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\to \left({1}^{st}\left({1}^{st}\left({T}\right)\right){+}_{f}\left(\left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]×\left\{1\right\}\right)\cup \left({2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left({M}+1\dots {N}\right)\right]×\left\{0\right\}\right)\right)\right)\left({y}\right)={1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)+1$
261 219 260 eqtrd ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\to {F}\left({M}\right)\left({y}\right)={1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)+1$
262 261 adantrr ${⊢}\left({\phi }\wedge \left({y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\wedge ¬{y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\right)\to {F}\left({M}\right)\left({y}\right)={1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)+1$
263 1 nngt0d ${⊢}{\phi }\to 0<{N}$
264 263 7 breqtrrd ${⊢}{\phi }\to 0<{2}^{nd}\left({U}\right)$
265 1 2 6 264 poimirlem5 ${⊢}{\phi }\to {F}\left(0\right)={1}^{st}\left({1}^{st}\left({U}\right)\right)$
266 263 5 breqtrrd ${⊢}{\phi }\to 0<{2}^{nd}\left({T}\right)$
267 1 2 4 266 poimirlem5 ${⊢}{\phi }\to {F}\left(0\right)={1}^{st}\left({1}^{st}\left({T}\right)\right)$
268 265 267 eqtr3d ${⊢}{\phi }\to {1}^{st}\left({1}^{st}\left({U}\right)\right)={1}^{st}\left({1}^{st}\left({T}\right)\right)$
269 268 fveq1d ${⊢}{\phi }\to {1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)={1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)$
270 269 adantr ${⊢}\left({\phi }\wedge \left({y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\wedge ¬{y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\right)\to {1}^{st}\left({1}^{st}\left({U}\right)\right)\left({y}\right)={1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)$
271 180 262 270 3eqtr3d ${⊢}\left({\phi }\wedge \left({y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\wedge ¬{y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\right)\to {1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)+1={1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)$
272 elmapi ${⊢}{1}^{st}\left({1}^{st}\left({T}\right)\right)\in \left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)\to {1}^{st}\left({1}^{st}\left({T}\right)\right):\left(1\dots {N}\right)⟶\left(0..^{K}\right)$
273 14 221 272 3syl ${⊢}{\phi }\to {1}^{st}\left({1}^{st}\left({T}\right)\right):\left(1\dots {N}\right)⟶\left(0..^{K}\right)$
274 273 ffvelrnda ${⊢}\left({\phi }\wedge {y}\in \left(1\dots {N}\right)\right)\to {1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)\in \left(0..^{K}\right)$
275 elfzonn0 ${⊢}{1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)\in \left(0..^{K}\right)\to {1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)\in {ℕ}_{0}$
276 274 275 syl ${⊢}\left({\phi }\wedge {y}\in \left(1\dots {N}\right)\right)\to {1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)\in {ℕ}_{0}$
277 276 nn0red ${⊢}\left({\phi }\wedge {y}\in \left(1\dots {N}\right)\right)\to {1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)\in ℝ$
278 277 ltp1d ${⊢}\left({\phi }\wedge {y}\in \left(1\dots {N}\right)\right)\to {1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)<{1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)+1$
279 277 278 gtned ${⊢}\left({\phi }\wedge {y}\in \left(1\dots {N}\right)\right)\to {1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)+1\ne {1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)$
280 220 279 syldan ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\to {1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)+1\ne {1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)$
281 280 neneqd ${⊢}\left({\phi }\wedge {y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\to ¬{1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)+1={1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)$
282 281 adantrr ${⊢}\left({\phi }\wedge \left({y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\wedge ¬{y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\right)\right)\to ¬{1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)+1={1}^{st}\left({1}^{st}\left({T}\right)\right)\left({y}\right)$
283 271 282 pm2.65da ${⊢}{\phi }\to ¬\left({y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\wedge ¬{y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\right)$
284 iman ${⊢}\left({y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\to {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\right)↔¬\left({y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\wedge ¬{y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\right)$
285 283 284 sylibr ${⊢}{\phi }\to \left({y}\in {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\to {y}\in {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]\right)$
286 285 ssrdv ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left({T}\right)\right)\left[\left(1\dots {M}\right)\right]\subseteq {2}^{nd}\left({1}^{st}\left({U}\right)\right)\left[\left(1\dots {M}\right)\right]$