Theorem poimirlem19

Description: Lemma for poimir establishing the vertices of the simplex in poimirlem20 . (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	poimir.0	$$⊢\phi \to N\in \mathbb{N}$$
	poimirlem22.s	$$⊢S=\left\{t\in \left(\left(\left({\left(0..^K\right)}^{\left(1\dots N\right)}\right)\times \left\{f|f:\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\right\}\right)\times \left(0\dots N\right)\right)|F=\left(y\in \left(0\dots N-1\right)⟼⦋if\left(y<2^{nd}\left(t\right),y,y+1\right)/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(t\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)\right)\right\}$$
	poimirlem22.1	$$⊢\phi \to F:\left(0\dots N-1\right)⟶{\left(0\dots K\right)}^{\left(1\dots N\right)}$$
	poimirlem22.2	$$⊢\phi \to T\in S$$
	poimirlem22.3	$$⊢\left(\phi \wedge n\in \left(1\dots N\right)\right)\to \exists p\in \mathrm{ran}Fp\left(n\right)\ne 0$$
	poimirlem21.4	$$⊢\phi \to 2^{nd}\left(T\right)=N$$
Assertion	poimirlem19	$$⊢\phi \to F=\left(y\in \left(0\dots N-1\right)⟼\left(n\in \left(1\dots N\right)⟼1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)\right){+}_f\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$$⊢\phi \to N\in \mathbb{N}$$
2		poimirlem22.s	$$⊢S=\left\{t\in \left(\left(\left({\left(0..^K\right)}^{\left(1\dots N\right)}\right)\times \left\{f|f:\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\right\}\right)\times \left(0\dots N\right)\right)|F=\left(y\in \left(0\dots N-1\right)⟼⦋if\left(y<2^{nd}\left(t\right),y,y+1\right)/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(t\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)\right)\right\}$$
3		poimirlem22.1	$$⊢\phi \to F:\left(0\dots N-1\right)⟶{\left(0\dots K\right)}^{\left(1\dots N\right)}$$
4		poimirlem22.2	$$⊢\phi \to T\in S$$
5		poimirlem22.3	$$⊢\left(\phi \wedge n\in \left(1\dots N\right)\right)\to \exists p\in \mathrm{ran}Fp\left(n\right)\ne 0$$
6		poimirlem21.4	$$⊢\phi \to 2^{nd}\left(T\right)=N$$
7		fveq2	$$⊢t=T\to 2^{nd}\left(t\right)=2^{nd}\left(T\right)$$
8	7	breq2d	$$⊢t=T\to \left(y<2^{nd}\left(t\right)\leftrightarrow y<2^{nd}\left(T\right)\right)$$
9	8	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)$$
10		2fveq3	$$⊢t=T\to 1^{st}\left(1^{st}\left(t\right)\right)=1^{st}\left(1^{st}\left(T\right)\right)$$
11		2fveq3	$$⊢t=T\to 2^{nd}\left(1^{st}\left(t\right)\right)=2^{nd}\left(1^{st}\left(T\right)\right)$$
12	11	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]$$
13	12	xpeq1d	$$⊢t=T\to 2^{nd}\left(1^{st}\left(t\right)\right)\left[\left(1\dots j\right)\right]\times \left\{1\right\}=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots j\right)\right]\times \left\{1\right\}$$
14	11	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]$$
15	14	xpeq1d	$$⊢t=T\to 2^{nd}\left(1^{st}\left(t\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}$$
16	13 15	uneq12d	$$⊢t=T\to \left(2^{nd}\left(1^{st}\left(t\right)\right)\left[\left(1\dots j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(t\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)=\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)$$
17	10 16	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]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(t\right)\right)\left[\left(j+1\dots N\right)\right]\times \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]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)$$
18	9 17	csbeq12dv	$$⊢t=T\to ⦋if\left(y<2^{nd}\left(t\right),y,y+1\right)/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(t\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)=⦋if\left(y<2^{nd}\left(T\right),y,y+1\right)/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)$$
19	18	mpteq2dv	$$⊢t=T\to \left(y\in \left(0\dots N-1\right)⟼⦋if\left(y<2^{nd}\left(t\right),y,y+1\right)/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(t\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)\right)=\left(y\in \left(0\dots N-1\right)⟼⦋if\left(y<2^{nd}\left(T\right),y,y+1\right)/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)\right)$$
20	19	eqeq2d	$$⊢t=T\to \left(F=\left(y\in \left(0\dots N-1\right)⟼⦋if\left(y<2^{nd}\left(t\right),y,y+1\right)/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(t\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)\right)\leftrightarrow F=\left(y\in \left(0\dots N-1\right)⟼⦋if\left(y<2^{nd}\left(T\right),y,y+1\right)/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)\right)\right)$$
21	20 2	elrab2	$$⊢T\in S\leftrightarrow \left(T\in \left(\left(\left({\left(0..^K\right)}^{\left(1\dots N\right)}\right)\times \left\{f|f:\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\right\}\right)\times \left(0\dots N\right)\right)\wedge F=\left(y\in \left(0\dots N-1\right)⟼⦋if\left(y<2^{nd}\left(T\right),y,y+1\right)/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)\right)\right)$$
22	21	simprbi	$$⊢T\in S\to F=\left(y\in \left(0\dots N-1\right)⟼⦋if\left(y<2^{nd}\left(T\right),y,y+1\right)/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)\right)$$
23	4 22	syl	$$⊢\phi \to F=\left(y\in \left(0\dots N-1\right)⟼⦋if\left(y<2^{nd}\left(T\right),y,y+1\right)/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)\right)$$
24		elrabi	$$⊢T\in \left\{t\in \left(\left(\left({\left(0..^K\right)}^{\left(1\dots N\right)}\right)\times \left\{f|f:\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\right\}\right)\times \left(0\dots N\right)\right)|F=\left(y\in \left(0\dots N-1\right)⟼⦋if\left(y<2^{nd}\left(t\right),y,y+1\right)/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(t\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)\right)\right\}\to T\in \left(\left(\left({\left(0..^K\right)}^{\left(1\dots N\right)}\right)\times \left\{f|f:\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\right\}\right)\times \left(0\dots N\right)\right)$$
25	24 2	eleq2s	$$⊢T\in S\to T\in \left(\left(\left({\left(0..^K\right)}^{\left(1\dots N\right)}\right)\times \left\{f|f:\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\right\}\right)\times \left(0\dots N\right)\right)$$
26	4 25	syl	$$⊢\phi \to T\in \left(\left(\left({\left(0..^K\right)}^{\left(1\dots N\right)}\right)\times \left\{f|f:\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\right\}\right)\times \left(0\dots N\right)\right)$$
27		xp1st	$$⊢T\in \left(\left(\left({\left(0..^K\right)}^{\left(1\dots N\right)}\right)\times \left\{f|f:\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\right\}\right)\times \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)\times \left\{f|f:\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\right\}\right)$$
28	26 27	syl	$$⊢\phi \to 1^{st}\left(T\right)\in \left(\left({\left(0..^K\right)}^{\left(1\dots N\right)}\right)\times \left\{f|f:\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\right\}\right)$$
29		xp1st	$$⊢1^{st}\left(T\right)\in \left(\left({\left(0..^K\right)}^{\left(1\dots N\right)}\right)\times \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)$$
30	28 29	syl	$$⊢\phi \to 1^{st}\left(1^{st}\left(T\right)\right)\in \left({\left(0..^K\right)}^{\left(1\dots N\right)}\right)$$
31		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)$$
32	30 31	syl	$$⊢\phi \to 1^{st}\left(1^{st}\left(T\right)\right)Fn\left(1\dots N\right)$$
33	32	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 1^{st}\left(1^{st}\left(T\right)\right)Fn\left(1\dots N\right)$$
34		1ex	$$⊢1\in \mathrm{V}$$
35		fnconstg	$$⊢1\in \mathrm{V}\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)Fn{2}^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]$$
36	34 35	ax-mp	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)Fn{2}^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]$$
37		c0ex	$$⊢0\in \mathrm{V}$$
38		fnconstg	$$⊢0\in \mathrm{V}\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)Fn{2}^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]$$
39	37 38	ax-mp	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)Fn{2}^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]$$
40	36 39	pm3.2i	$$⊢\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)Fn{2}^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\wedge \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)Fn{2}^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\right)$$
41		xp2nd	$$⊢1^{st}\left(T\right)\in \left(\left({\left(0..^K\right)}^{\left(1\dots N\right)}\right)\times \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\}$$
42	28 41	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\}$$
43		fvex	$$⊢2^{nd}\left(1^{st}\left(T\right)\right)\in \mathrm{V}$$
44		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)\leftrightarrow 2^{nd}\left(1^{st}\left(T\right)\right):\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\right)$$
45	43 44	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\}\leftrightarrow 2^{nd}\left(1^{st}\left(T\right)\right):\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)$$
46	42 45	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)$$
47		dff1o3	$$⊢2^{nd}\left(1^{st}\left(T\right)\right):\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\leftrightarrow \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)$$
48	47	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}$$
49	46 48	syl	$$⊢\phi \to \mathrm{Fun}{2^{nd}\left(1^{st}\left(T\right)\right)}^{-1}$$
50		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 y\right)\cap \left(y+1\dots N\right)\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cap 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]$$
51	49 50	syl	$$⊢\phi \to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\cap \left(y+1\dots N\right)\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cap 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]$$
52		elfznn0	$$⊢y\in \left(0\dots N-1\right)\to y\in {\mathbb{N}}_0$$
53	52	nn0red	$$⊢y\in \left(0\dots N-1\right)\to y\in ℝ$$
54	53	ltp1d	$$⊢y\in \left(0\dots N-1\right)\to y<y+1$$
55		fzdisj	$$⊢y<y+1\to \left(1\dots y\right)\cap \left(y+1\dots N\right)=\varnothing$$
56	54 55	syl	$$⊢y\in \left(0\dots N-1\right)\to \left(1\dots y\right)\cap \left(y+1\dots N\right)=\varnothing$$
57	56	imaeq2d	$$⊢y\in \left(0\dots N-1\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\cap \left(y+1\dots N\right)\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\varnothing \right]$$
58		ima0	$$⊢2^{nd}\left(1^{st}\left(T\right)\right)\left[\varnothing \right]=\varnothing$$
59	57 58	eqtrdi	$$⊢y\in \left(0\dots N-1\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\cap \left(y+1\dots N\right)\right]=\varnothing$$
60	51 59	sylan9req	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cap 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]=\varnothing$$
61		fnun	$$⊢\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)Fn{2}^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\wedge \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)Fn{2}^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\right)\wedge 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cap 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]=\varnothing \right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)Fn\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cup 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\right)$$
62	40 60 61	sylancr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)Fn\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cup 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\right)$$
63		imaundi	$$⊢2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\cup \left(y+1\dots N\right)\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cup 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]$$
64		nn0p1nn	$$⊢y\in {\mathbb{N}}_0\to y+1\in \mathbb{N}$$
65	52 64	syl	$$⊢y\in \left(0\dots N-1\right)\to y+1\in \mathbb{N}$$
66		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
67	65 66	eleqtrdi	$$⊢y\in \left(0\dots N-1\right)\to y+1\in {\mathbb{Z}}_{\ge 1}$$
68	67	adantl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to y+1\in {\mathbb{Z}}_{\ge 1}$$
69	1	nncnd	$$⊢\phi \to N\in ℂ$$
70		npcan1	$$⊢N\in ℂ\to N-1+1=N$$
71	69 70	syl	$$⊢\phi \to N-1+1=N$$
72	71	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to N-1+1=N$$
73		elfzuz3	$$⊢y\in \left(0\dots N-1\right)\to N-1\in {\mathbb{Z}}_{\ge y}$$
74		peano2uz	$$⊢N-1\in {\mathbb{Z}}_{\ge y}\to N-1+1\in {\mathbb{Z}}_{\ge y}$$
75	73 74	syl	$$⊢y\in \left(0\dots N-1\right)\to N-1+1\in {\mathbb{Z}}_{\ge y}$$
76	75	adantl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to N-1+1\in {\mathbb{Z}}_{\ge y}$$
77	72 76	eqeltrrd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to N\in {\mathbb{Z}}_{\ge y}$$
78		fzsplit2	$$⊢\left(y+1\in {\mathbb{Z}}_{\ge 1}\wedge N\in {\mathbb{Z}}_{\ge y}\right)\to \left(1\dots N\right)=\left(1\dots y\right)\cup \left(y+1\dots N\right)$$
79	68 77 78	syl2anc	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(1\dots N\right)=\left(1\dots y\right)\cup \left(y+1\dots N\right)$$
80	79	imaeq2d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\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 y\right)\cup \left(y+1\dots N\right)\right]$$
81		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)$$
82		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)$$
83	46 81 82	3syl	$$⊢\phi \to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]=\left(1\dots N\right)$$
84	83	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]=\left(1\dots N\right)$$
85	80 84	eqtr3d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\cup \left(y+1\dots N\right)\right]=\left(1\dots N\right)$$
86	63 85	eqtr3id	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cup 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]=\left(1\dots N\right)$$
87	86	fneq2d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)Fn\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cup 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\right)\leftrightarrow \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)Fn\left(1\dots N\right)\right)$$
88	62 87	mpbid	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)Fn\left(1\dots N\right)$$
89		ovexd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(1\dots N\right)\in \mathrm{V}$$
90		inidm	$$⊢\left(1\dots N\right)\cap \left(1\dots N\right)=\left(1\dots N\right)$$
91		eqidd	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\to 1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)=1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)$$
92		eqidd	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)$$
93	33 88 89 89 90 91 92	offval	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\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 y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)=\left(n\in \left(1\dots N\right)⟼1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)+\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)\right)$$
94		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)$$
95	30 94	syl	$$⊢\phi \to 1^{st}\left(1^{st}\left(T\right)\right):\left(1\dots N\right)⟶\left(0..^K\right)$$
96	95	ffvelcdmda	$$⊢\left(\phi \wedge n\in \left(1\dots N\right)\right)\to 1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)\in \left(0..^K\right)$$
97		elfzonn0	$$⊢1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)\in \left(0..^K\right)\to 1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)\in {\mathbb{N}}_0$$
98	96 97	syl	$$⊢\left(\phi \wedge n\in \left(1\dots N\right)\right)\to 1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)\in {\mathbb{N}}_0$$
99	98	nn0cnd	$$⊢\left(\phi \wedge n\in \left(1\dots N\right)\right)\to 1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)\in ℂ$$
100	99	adantlr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\to 1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)\in ℂ$$
101		ax-1cn	$$⊢1\in ℂ$$
102		0cn	$$⊢0\in ℂ$$
103	101 102	ifcli	$$⊢if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)\in ℂ$$
104	103	a1i	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\to if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)\in ℂ$$
105		snssi	$$⊢1\in ℂ\to \left\{1\right\}\subseteq ℂ$$
106	101 105	ax-mp	$$⊢\left\{1\right\}\subseteq ℂ$$
107		snssi	$$⊢0\in ℂ\to \left\{0\right\}\subseteq ℂ$$
108	102 107	ax-mp	$$⊢\left\{0\right\}\subseteq ℂ$$
109	106 108	unssi	$$⊢\left\{1\right\}\cup \left\{0\right\}\subseteq ℂ$$
110	34	fconst	$$⊢\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right):\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]⟶\left\{1\right\}$$
111	37	fconst	$$⊢\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right):\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]⟶\left\{0\right\}$$
112	110 111	pm3.2i	$$⊢\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right):\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]⟶\left\{1\right\}\wedge \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right):\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]⟶\left\{0\right\}\right)$$
113		simpr	$$⊢\left(\phi \wedge n\in \left(1+1\dots N\right)\right)\to n\in \left(1+1\dots N\right)$$
114	1	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
115		1z	$$⊢1\in \mathbb{Z}$$
116		peano2z	$$⊢1\in \mathbb{Z}\to 1+1\in \mathbb{Z}$$
117	115 116	ax-mp	$$⊢1+1\in \mathbb{Z}$$
118	114 117	jctil	$$⊢\phi \to \left(1+1\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)$$
119		elfzelz	$$⊢n\in \left(1+1\dots N\right)\to n\in \mathbb{Z}$$
120	119 115	jctir	$$⊢n\in \left(1+1\dots N\right)\to \left(n\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)$$
121		fzsubel	$$⊢\left(\left(1+1\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\wedge \left(n\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)\right)\to \left(n\in \left(1+1\dots N\right)\leftrightarrow n-1\in \left(1+1-1\dots N-1\right)\right)$$
122	118 120 121	syl2an	$$⊢\left(\phi \wedge n\in \left(1+1\dots N\right)\right)\to \left(n\in \left(1+1\dots N\right)\leftrightarrow n-1\in \left(1+1-1\dots N-1\right)\right)$$
123	113 122	mpbid	$$⊢\left(\phi \wedge n\in \left(1+1\dots N\right)\right)\to n-1\in \left(1+1-1\dots N-1\right)$$
124	101 101	pncan3oi	$$⊢1+1-1=1$$
125	124	oveq1i	$$⊢\left(1+1-1\dots N-1\right)=\left(1\dots N-1\right)$$
126	123 125	eleqtrdi	$$⊢\left(\phi \wedge n\in \left(1+1\dots N\right)\right)\to n-1\in \left(1\dots N-1\right)$$
127	126	ralrimiva	$$⊢\phi \to \forall n\in \left(1+1\dots N\right)n-1\in \left(1\dots N-1\right)$$
128		simpr	$$⊢\left(\phi \wedge y\in \left(1\dots N-1\right)\right)\to y\in \left(1\dots N-1\right)$$
129		peano2zm	$$⊢N\in \mathbb{Z}\to N-1\in \mathbb{Z}$$
130	114 129	syl	$$⊢\phi \to N-1\in \mathbb{Z}$$
131	130 115	jctil	$$⊢\phi \to \left(1\in \mathbb{Z}\wedge N-1\in \mathbb{Z}\right)$$
132		elfzelz	$$⊢y\in \left(1\dots N-1\right)\to y\in \mathbb{Z}$$
133	132 115	jctir	$$⊢y\in \left(1\dots N-1\right)\to \left(y\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)$$
134		fzaddel	$$⊢\left(\left(1\in \mathbb{Z}\wedge N-1\in \mathbb{Z}\right)\wedge \left(y\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)\right)\to \left(y\in \left(1\dots N-1\right)\leftrightarrow y+1\in \left(1+1\dots N-1+1\right)\right)$$
135	131 133 134	syl2an	$$⊢\left(\phi \wedge y\in \left(1\dots N-1\right)\right)\to \left(y\in \left(1\dots N-1\right)\leftrightarrow y+1\in \left(1+1\dots N-1+1\right)\right)$$
136	128 135	mpbid	$$⊢\left(\phi \wedge y\in \left(1\dots N-1\right)\right)\to y+1\in \left(1+1\dots N-1+1\right)$$
137	71	oveq2d	$$⊢\phi \to \left(1+1\dots N-1+1\right)=\left(1+1\dots N\right)$$
138	137	adantr	$$⊢\left(\phi \wedge y\in \left(1\dots N-1\right)\right)\to \left(1+1\dots N-1+1\right)=\left(1+1\dots N\right)$$
139	136 138	eleqtrd	$$⊢\left(\phi \wedge y\in \left(1\dots N-1\right)\right)\to y+1\in \left(1+1\dots N\right)$$
140	119	zcnd	$$⊢n\in \left(1+1\dots N\right)\to n\in ℂ$$
141	132	zcnd	$$⊢y\in \left(1\dots N-1\right)\to y\in ℂ$$
142		subadd2	$$⊢\left(n\in ℂ\wedge 1\in ℂ\wedge y\in ℂ\right)\to \left(n-1=y\leftrightarrow y+1=n\right)$$
143	101 142	mp3an2	$$⊢\left(n\in ℂ\wedge y\in ℂ\right)\to \left(n-1=y\leftrightarrow y+1=n\right)$$
144		eqcom	$$⊢y=n-1\leftrightarrow n-1=y$$
145		eqcom	$$⊢n=y+1\leftrightarrow y+1=n$$
146	143 144 145	3bitr4g	$$⊢\left(n\in ℂ\wedge y\in ℂ\right)\to \left(y=n-1\leftrightarrow n=y+1\right)$$
147	140 141 146	syl2anr	$$⊢\left(y\in \left(1\dots N-1\right)\wedge n\in \left(1+1\dots N\right)\right)\to \left(y=n-1\leftrightarrow n=y+1\right)$$
148	147	ralrimiva	$$⊢y\in \left(1\dots N-1\right)\to \forall n\in \left(1+1\dots N\right)\left(y=n-1\leftrightarrow n=y+1\right)$$
149	148	adantl	$$⊢\left(\phi \wedge y\in \left(1\dots N-1\right)\right)\to \forall n\in \left(1+1\dots N\right)\left(y=n-1\leftrightarrow n=y+1\right)$$
150		reu6i	$$⊢\left(y+1\in \left(1+1\dots N\right)\wedge \forall n\in \left(1+1\dots N\right)\left(y=n-1\leftrightarrow n=y+1\right)\right)\to \exists !n\in \left(1+1\dots N\right)y=n-1$$
151	139 149 150	syl2anc	$$⊢\left(\phi \wedge y\in \left(1\dots N-1\right)\right)\to \exists !n\in \left(1+1\dots N\right)y=n-1$$
152	151	ralrimiva	$$⊢\phi \to \forall y\in \left(1\dots N-1\right)\exists !n\in \left(1+1\dots N\right)y=n-1$$
153		eqid	$$⊢\left(n\in \left(1+1\dots N\right)⟼n-1\right)=\left(n\in \left(1+1\dots N\right)⟼n-1\right)$$
154	153	f1ompt	$$⊢\left(n\in \left(1+1\dots N\right)⟼n-1\right):\left(1+1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N-1\right)\leftrightarrow \left(\forall n\in \left(1+1\dots N\right)n-1\in \left(1\dots N-1\right)\wedge \forall y\in \left(1\dots N-1\right)\exists !n\in \left(1+1\dots N\right)y=n-1\right)$$
155	127 152 154	sylanbrc	$$⊢\phi \to \left(n\in \left(1+1\dots N\right)⟼n-1\right):\left(1+1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N-1\right)$$
156		f1osng	$$⊢\left(1\in \mathrm{V}\wedge N\in \mathbb{N}\right)\to \left\{⟨1,N⟩\right\}:\left\{1\right\}\underset{1-1\; onto}{⟶}\left\{N\right\}$$
157	34 1 156	sylancr	$$⊢\phi \to \left\{⟨1,N⟩\right\}:\left\{1\right\}\underset{1-1\; onto}{⟶}\left\{N\right\}$$
158	1	nnred	$$⊢\phi \to N\in ℝ$$
159	158	ltm1d	$$⊢\phi \to N-1<N$$
160	130	zred	$$⊢\phi \to N-1\in ℝ$$
161	160 158	ltnled	$$⊢\phi \to \left(N-1<N\leftrightarrow \neg N\le N-1\right)$$
162	159 161	mpbid	$$⊢\phi \to \neg N\le N-1$$
163		elfzle2	$$⊢N\in \left(1\dots N-1\right)\to N\le N-1$$
164	162 163	nsyl	$$⊢\phi \to \neg N\in \left(1\dots N-1\right)$$
165		disjsn	$$⊢\left(1\dots N-1\right)\cap \left\{N\right\}=\varnothing \leftrightarrow \neg N\in \left(1\dots N-1\right)$$
166	164 165	sylibr	$$⊢\phi \to \left(1\dots N-1\right)\cap \left\{N\right\}=\varnothing$$
167		1re	$$⊢1\in ℝ$$
168	167	ltp1i	$$⊢1<1+1$$
169	117	zrei	$$⊢1+1\in ℝ$$
170	167 169	ltnlei	$$⊢1<1+1\leftrightarrow \neg 1+1\le 1$$
171	168 170	mpbi	$$⊢\neg 1+1\le 1$$
172		elfzle1	$$⊢1\in \left(1+1\dots N\right)\to 1+1\le 1$$
173	171 172	mto	$$⊢\neg 1\in \left(1+1\dots N\right)$$
174		disjsn	$$⊢\left(1+1\dots N\right)\cap \left\{1\right\}=\varnothing \leftrightarrow \neg 1\in \left(1+1\dots N\right)$$
175	173 174	mpbir	$$⊢\left(1+1\dots N\right)\cap \left\{1\right\}=\varnothing$$
176		f1oun	$$⊢\left(\left(\left(n\in \left(1+1\dots N\right)⟼n-1\right):\left(1+1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N-1\right)\wedge \left\{⟨1,N⟩\right\}:\left\{1\right\}\underset{1-1\; onto}{⟶}\left\{N\right\}\right)\wedge \left(\left(1+1\dots N\right)\cap \left\{1\right\}=\varnothing \wedge \left(1\dots N-1\right)\cap \left\{N\right\}=\varnothing \right)\right)\to \left(\left(n\in \left(1+1\dots N\right)⟼n-1\right)\cup \left\{⟨1,N⟩\right\}\right):\left(1+1\dots N\right)\cup \left\{1\right\}\underset{1-1\; onto}{⟶}\left(1\dots N-1\right)\cup \left\{N\right\}$$
177	175 176	mpanr1	$$⊢\left(\left(\left(n\in \left(1+1\dots N\right)⟼n-1\right):\left(1+1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N-1\right)\wedge \left\{⟨1,N⟩\right\}:\left\{1\right\}\underset{1-1\; onto}{⟶}\left\{N\right\}\right)\wedge \left(1\dots N-1\right)\cap \left\{N\right\}=\varnothing \right)\to \left(\left(n\in \left(1+1\dots N\right)⟼n-1\right)\cup \left\{⟨1,N⟩\right\}\right):\left(1+1\dots N\right)\cup \left\{1\right\}\underset{1-1\; onto}{⟶}\left(1\dots N-1\right)\cup \left\{N\right\}$$
178	155 157 166 177	syl21anc	$$⊢\phi \to \left(\left(n\in \left(1+1\dots N\right)⟼n-1\right)\cup \left\{⟨1,N⟩\right\}\right):\left(1+1\dots N\right)\cup \left\{1\right\}\underset{1-1\; onto}{⟶}\left(1\dots N-1\right)\cup \left\{N\right\}$$
179		eleq1	$$⊢n=1\to \left(n\in \left(1+1\dots N\right)\leftrightarrow 1\in \left(1+1\dots N\right)\right)$$
180	173 179	mtbiri	$$⊢n=1\to \neg n\in \left(1+1\dots N\right)$$
181	180	necon2ai	$$⊢n\in \left(1+1\dots N\right)\to n\ne 1$$
182		ifnefalse	$$⊢n\ne 1\to if\left(n=1,N,n-1\right)=n-1$$
183	181 182	syl	$$⊢n\in \left(1+1\dots N\right)\to if\left(n=1,N,n-1\right)=n-1$$
184	183	mpteq2ia	$$⊢\left(n\in \left(1+1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)=\left(n\in \left(1+1\dots N\right)⟼n-1\right)$$
185	184	uneq1i	$$⊢\left(n\in \left(1+1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\cup \left\{⟨1,N⟩\right\}=\left(n\in \left(1+1\dots N\right)⟼n-1\right)\cup \left\{⟨1,N⟩\right\}$$
186	34	a1i	$$⊢\phi \to 1\in \mathrm{V}$$
187	1 66	eleqtrdi	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 1}$$
188		fzpred	$$⊢N\in {\mathbb{Z}}_{\ge 1}\to \left(1\dots N\right)=\left\{1\right\}\cup \left(1+1\dots N\right)$$
189	187 188	syl	$$⊢\phi \to \left(1\dots N\right)=\left\{1\right\}\cup \left(1+1\dots N\right)$$
190		uncom	$$⊢\left\{1\right\}\cup \left(1+1\dots N\right)=\left(1+1\dots N\right)\cup \left\{1\right\}$$
191	189 190	eqtr2di	$$⊢\phi \to \left(1+1\dots N\right)\cup \left\{1\right\}=\left(1\dots N\right)$$
192		iftrue	$$⊢n=1\to if\left(n=1,N,n-1\right)=N$$
193	192	adantl	$$⊢\left(\phi \wedge n=1\right)\to if\left(n=1,N,n-1\right)=N$$
194	186 1 191 193	fmptapd	$$⊢\phi \to \left(n\in \left(1+1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\cup \left\{⟨1,N⟩\right\}=\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)$$
195	185 194	eqtr3id	$$⊢\phi \to \left(n\in \left(1+1\dots N\right)⟼n-1\right)\cup \left\{⟨1,N⟩\right\}=\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)$$
196	71 187	eqeltrd	$$⊢\phi \to N-1+1\in {\mathbb{Z}}_{\ge 1}$$
197		uzid	$$⊢N-1\in \mathbb{Z}\to N-1\in {\mathbb{Z}}_{\ge \left(N-1\right)}$$
198		peano2uz	$$⊢N-1\in {\mathbb{Z}}_{\ge \left(N-1\right)}\to N-1+1\in {\mathbb{Z}}_{\ge \left(N-1\right)}$$
199	130 197 198	3syl	$$⊢\phi \to N-1+1\in {\mathbb{Z}}_{\ge \left(N-1\right)}$$
200	71 199	eqeltrrd	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge \left(N-1\right)}$$
201		fzsplit2	$$⊢\left(N-1+1\in {\mathbb{Z}}_{\ge 1}\wedge N\in {\mathbb{Z}}_{\ge \left(N-1\right)}\right)\to \left(1\dots N\right)=\left(1\dots N-1\right)\cup \left(N-1+1\dots N\right)$$
202	196 200 201	syl2anc	$$⊢\phi \to \left(1\dots N\right)=\left(1\dots N-1\right)\cup \left(N-1+1\dots N\right)$$
203	71	oveq1d	$$⊢\phi \to \left(N-1+1\dots N\right)=\left(N\dots N\right)$$
204		fzsn	$$⊢N\in \mathbb{Z}\to \left(N\dots N\right)=\left\{N\right\}$$
205	114 204	syl	$$⊢\phi \to \left(N\dots N\right)=\left\{N\right\}$$
206	203 205	eqtrd	$$⊢\phi \to \left(N-1+1\dots N\right)=\left\{N\right\}$$
207	206	uneq2d	$$⊢\phi \to \left(1\dots N-1\right)\cup \left(N-1+1\dots N\right)=\left(1\dots N-1\right)\cup \left\{N\right\}$$
208	202 207	eqtr2d	$$⊢\phi \to \left(1\dots N-1\right)\cup \left\{N\right\}=\left(1\dots N\right)$$
209	195 191 208	f1oeq123d	$$⊢\phi \to \left(\left(\left(n\in \left(1+1\dots N\right)⟼n-1\right)\cup \left\{⟨1,N⟩\right\}\right):\left(1+1\dots N\right)\cup \left\{1\right\}\underset{1-1\; onto}{⟶}\left(1\dots N-1\right)\cup \left\{N\right\}\leftrightarrow \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right):\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\right)$$
210	178 209	mpbid	$$⊢\phi \to \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right):\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)$$
211		f1oco	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right):\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\wedge \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right):\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right):\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)$$
212	46 210 211	syl2anc	$$⊢\phi \to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right):\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)$$
213		dff1o3	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right):\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\leftrightarrow \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right):\left(1\dots N\right)\underset{onto}{⟶}\left(1\dots N\right)\wedge \mathrm{Fun}{\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)}^{-1}\right)$$
214	213	simprbi	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right):\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\to \mathrm{Fun}{\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)}^{-1}$$
215		imain	$$⊢\mathrm{Fun}{\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)}^{-1}\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\cap \left(y+1+1\dots N\right)\right]=\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\cap \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]$$
216	212 214 215	3syl	$$⊢\phi \to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\cap \left(y+1+1\dots N\right)\right]=\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\cap \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]$$
217	65	nnred	$$⊢y\in \left(0\dots N-1\right)\to y+1\in ℝ$$
218	217	ltp1d	$$⊢y\in \left(0\dots N-1\right)\to y+1<y+1+1$$
219		fzdisj	$$⊢y+1<y+1+1\to \left(1\dots y+1\right)\cap \left(y+1+1\dots N\right)=\varnothing$$
220	218 219	syl	$$⊢y\in \left(0\dots N-1\right)\to \left(1\dots y+1\right)\cap \left(y+1+1\dots N\right)=\varnothing$$
221	220	imaeq2d	$$⊢y\in \left(0\dots N-1\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\cap \left(y+1+1\dots N\right)\right]=\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\varnothing \right]$$
222		ima0	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\varnothing \right]=\varnothing$$
223	221 222	eqtrdi	$$⊢y\in \left(0\dots N-1\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\cap \left(y+1+1\dots N\right)\right]=\varnothing$$
224	216 223	sylan9req	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\cap \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]=\varnothing$$
225		fun	$$⊢\left(\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right):\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]⟶\left\{1\right\}\wedge \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right):\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]⟶\left\{0\right\}\right)\wedge \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\cap \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]=\varnothing \right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right):\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]⟶\left\{1\right\}\cup \left\{0\right\}$$
226	112 224 225	sylancr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right):\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]⟶\left\{1\right\}\cup \left\{0\right\}$$
227		imaundi	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\cup \left(y+1+1\dots N\right)\right]=\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]$$
228	65	peano2nnd	$$⊢y\in \left(0\dots N-1\right)\to y+1+1\in \mathbb{N}$$
229	228 66	eleqtrdi	$$⊢y\in \left(0\dots N-1\right)\to y+1+1\in {\mathbb{Z}}_{\ge 1}$$
230	229	adantl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to y+1+1\in {\mathbb{Z}}_{\ge 1}$$
231		eluzp1p1	$$⊢N-1\in {\mathbb{Z}}_{\ge y}\to N-1+1\in {\mathbb{Z}}_{\ge \left(y+1\right)}$$
232	73 231	syl	$$⊢y\in \left(0\dots N-1\right)\to N-1+1\in {\mathbb{Z}}_{\ge \left(y+1\right)}$$
233	232	adantl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to N-1+1\in {\mathbb{Z}}_{\ge \left(y+1\right)}$$
234	72 233	eqeltrrd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to N\in {\mathbb{Z}}_{\ge \left(y+1\right)}$$
235		fzsplit2	$$⊢\left(y+1+1\in {\mathbb{Z}}_{\ge 1}\wedge N\in {\mathbb{Z}}_{\ge \left(y+1\right)}\right)\to \left(1\dots N\right)=\left(1\dots y+1\right)\cup \left(y+1+1\dots N\right)$$
236	230 234 235	syl2anc	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(1\dots N\right)=\left(1\dots y+1\right)\cup \left(y+1+1\dots N\right)$$
237	236	imaeq2d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots N\right)\right]=\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\cup \left(y+1+1\dots N\right)\right]$$
238		f1ofo	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right):\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right):\left(1\dots N\right)\underset{onto}{⟶}\left(1\dots N\right)$$
239		foima	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right):\left(1\dots N\right)\underset{onto}{⟶}\left(1\dots N\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots N\right)\right]=\left(1\dots N\right)$$
240	212 238 239	3syl	$$⊢\phi \to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots N\right)\right]=\left(1\dots N\right)$$
241	240	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots N\right)\right]=\left(1\dots N\right)$$
242	237 241	eqtr3d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\cup \left(y+1+1\dots N\right)\right]=\left(1\dots N\right)$$
243	227 242	eqtr3id	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]=\left(1\dots N\right)$$
244	243	feq2d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right):\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]⟶\left\{1\right\}\cup \left\{0\right\}\leftrightarrow \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right):\left(1\dots N\right)⟶\left\{1\right\}\cup \left\{0\right\}\right)$$
245	226 244	mpbid	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right):\left(1\dots N\right)⟶\left\{1\right\}\cup \left\{0\right\}$$
246	245	ffvelcdmda	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)\in \left(\left\{1\right\}\cup \left\{0\right\}\right)$$
247	109 246	sselid	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)\in ℂ$$
248	100 104 247	subadd23d	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\to 1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)+\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)=1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)+\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)$$
249		oveq2	$$⊢1=if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-1=\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)$$
250	249	eqeq1d	$$⊢1=if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)\to \left(\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-1=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)\leftrightarrow \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)\right)$$
251		oveq2	$$⊢0=if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-0=\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)$$
252	251	eqeq1d	$$⊢0=if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)\to \left(\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-0=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)\leftrightarrow \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)\right)$$
253		1m1e0	$$⊢1-1=0$$
254		f1ofn	$$⊢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)Fn\left(1\dots N\right)$$
255	46 254	syl	$$⊢\phi \to 2^{nd}\left(1^{st}\left(T\right)\right)Fn\left(1\dots N\right)$$
256	255	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)Fn\left(1\dots N\right)$$
257		imassrn	$$⊢\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1\dots y+1\right)\right]\subseteq \mathrm{ran}\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)$$
258		f1of	$$⊢\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right):\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\to \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right):\left(1\dots N\right)⟶\left(1\dots N\right)$$
259	210 258	syl	$$⊢\phi \to \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right):\left(1\dots N\right)⟶\left(1\dots N\right)$$
260	259	frnd	$$⊢\phi \to \mathrm{ran}\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\subseteq \left(1\dots N\right)$$
261	257 260	sstrid	$$⊢\phi \to \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1\dots y+1\right)\right]\subseteq \left(1\dots N\right)$$
262	261	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1\dots y+1\right)\right]\subseteq \left(1\dots N\right)$$
263		eqidd	$$⊢\phi \to \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)=\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)$$
264		eluzfz1	$$⊢N\in {\mathbb{Z}}_{\ge 1}\to 1\in \left(1\dots N\right)$$
265	187 264	syl	$$⊢\phi \to 1\in \left(1\dots N\right)$$
266	263 193 265 1	fvmptd	$$⊢\phi \to \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left(1\right)=N$$
267	266	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left(1\right)=N$$
268		f1ofn	$$⊢\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right):\left(1\dots N\right)\underset{1-1\; onto}{⟶}\left(1\dots N\right)\to \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)Fn\left(1\dots N\right)$$
269	210 268	syl	$$⊢\phi \to \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)Fn\left(1\dots N\right)$$
270	269	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)Fn\left(1\dots N\right)$$
271		fzss2	$$⊢N\in {\mathbb{Z}}_{\ge \left(y+1\right)}\to \left(1\dots y+1\right)\subseteq \left(1\dots N\right)$$
272	234 271	syl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(1\dots y+1\right)\subseteq \left(1\dots N\right)$$
273		eluzfz1	$$⊢y+1\in {\mathbb{Z}}_{\ge 1}\to 1\in \left(1\dots y+1\right)$$
274	67 273	syl	$$⊢y\in \left(0\dots N-1\right)\to 1\in \left(1\dots y+1\right)$$
275	274	adantl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 1\in \left(1\dots y+1\right)$$
276		fnfvima	$$⊢\left(\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)Fn\left(1\dots N\right)\wedge \left(1\dots y+1\right)\subseteq \left(1\dots N\right)\wedge 1\in \left(1\dots y+1\right)\right)\to \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left(1\right)\in \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1\dots y+1\right)\right]$$
277	270 272 275 276	syl3anc	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left(1\right)\in \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1\dots y+1\right)\right]$$
278	267 277	eqeltrrd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to N\in \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1\dots y+1\right)\right]$$
279		fnfvima	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)Fn\left(1\dots N\right)\wedge \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1\dots y+1\right)\right]\subseteq \left(1\dots N\right)\wedge N\in \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1\dots y+1\right)\right]\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\in 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1\dots y+1\right)\right]\right]$$
280	256 262 278 279	syl3anc	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\in 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1\dots y+1\right)\right]\right]$$
281		imaco	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1\dots y+1\right)\right]\right]$$
282	280 281	eleqtrrdi	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\in \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]$$
283		fnconstg	$$⊢1\in \mathrm{V}\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)Fn\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]$$
284	34 283	ax-mp	$$⊢\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)Fn\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]$$
285		fnconstg	$$⊢0\in \mathrm{V}\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)Fn\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]$$
286	37 285	ax-mp	$$⊢\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)Fn\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]$$
287		fvun1	$$⊢\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)Fn\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\wedge \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)Fn\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\wedge \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\cap \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]=\varnothing \wedge 2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\in \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)$$
288	284 286 287	mp3an12	$$⊢\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\cap \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]=\varnothing \wedge 2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\in \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)$$
289	224 282 288	syl2anc	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)$$
290	34	fvconst2	$$⊢2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\in \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)=1$$
291	282 290	syl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)=1$$
292	289 291	eqtrd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)=1$$
293	292	oveq1d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)-1=1-1$$
294		fzss1	$$⊢y+1\in {\mathbb{Z}}_{\ge 1}\to \left(y+1\dots N\right)\subseteq \left(1\dots N\right)$$
295	67 294	syl	$$⊢y\in \left(0\dots N-1\right)\to \left(y+1\dots N\right)\subseteq \left(1\dots N\right)$$
296	295	adantl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(y+1\dots N\right)\subseteq \left(1\dots N\right)$$
297		eluzfz2	$$⊢N\in {\mathbb{Z}}_{\ge \left(y+1\right)}\to N\in \left(y+1\dots N\right)$$
298	234 297	syl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to N\in \left(y+1\dots N\right)$$
299		fnfvima	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)Fn\left(1\dots N\right)\wedge \left(y+1\dots N\right)\subseteq \left(1\dots N\right)\wedge N\in \left(y+1\dots N\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\in 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]$$
300	256 296 298 299	syl3anc	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\in 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]$$
301		fvun2	$$⊢\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)Fn{2}^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\wedge \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)Fn{2}^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\wedge \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cap 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]=\varnothing \wedge 2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\in 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\right)\right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)=\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)$$
302	36 39 301	mp3an12	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cap 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]=\varnothing \wedge 2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\in 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)=\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)$$
303	60 300 302	syl2anc	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)=\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)$$
304	37	fvconst2	$$⊢2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\in 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)=0$$
305	300 304	syl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)=0$$
306	303 305	eqtrd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)=0$$
307	253 293 306	3eqtr4a	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)-1=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)$$
308		fveq2	$$⊢n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)=\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)$$
309	308	oveq1d	$$⊢n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-1=\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)-1$$
310		fveq2	$$⊢n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)$$
311	309 310	eqeq12d	$$⊢n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\to \left(\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-1=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)\leftrightarrow \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)-1=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)\right)$$
312	307 311	syl5ibrcom	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-1=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)\right)$$
313	312	imp	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-1=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)$$
314	313	adantlr	$$⊢\left(\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\wedge n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-1=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)$$
315	247	subid1d	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-0=\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)$$
316	315	adantr	$$⊢\left(\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\wedge \neg n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-0=\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)$$
317		eldifsn	$$⊢n\in \left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\leftrightarrow \left(n\in \left(1\dots N\right)\wedge n\ne 2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)$$
318		df-ne	$$⊢n\ne 2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\leftrightarrow \neg n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)$$
319	318	anbi2i	$$⊢\left(n\in \left(1\dots N\right)\wedge n\ne 2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)\leftrightarrow \left(n\in \left(1\dots N\right)\wedge \neg n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)$$
320	317 319	bitri	$$⊢n\in \left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\leftrightarrow \left(n\in \left(1\dots N\right)\wedge \neg n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)$$
321		fnconstg	$$⊢0\in \mathrm{V}\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)Fn{2}^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]$$
322	37 321	ax-mp	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)Fn{2}^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]$$
323	36 322	pm3.2i	$$⊢\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)Fn{2}^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\wedge \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)Fn{2}^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\right)$$
324		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 y\right)\cap \left(y+1\dots N-1\right)\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cap 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]$$
325	49 324	syl	$$⊢\phi \to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\cap \left(y+1\dots N-1\right)\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cap 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]$$
326		fzdisj	$$⊢y<y+1\to \left(1\dots y\right)\cap \left(y+1\dots N-1\right)=\varnothing$$
327	54 326	syl	$$⊢y\in \left(0\dots N-1\right)\to \left(1\dots y\right)\cap \left(y+1\dots N-1\right)=\varnothing$$
328	327	imaeq2d	$$⊢y\in \left(0\dots N-1\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\cap \left(y+1\dots N-1\right)\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\varnothing \right]$$
329	328 58	eqtrdi	$$⊢y\in \left(0\dots N-1\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\cap \left(y+1\dots N-1\right)\right]=\varnothing$$
330	325 329	sylan9req	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cap 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]=\varnothing$$
331		fnun	$$⊢\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)Fn{2}^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\wedge \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)Fn{2}^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\right)\wedge 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cap 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]=\varnothing \right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)Fn\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cup 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\right)$$
332	323 330 331	sylancr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)Fn\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cup 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\right)$$
333		imaundi	$$⊢2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\cup \left(y+1\dots N-1\right)\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cup 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]$$
334	202 207	eqtrd	$$⊢\phi \to \left(1\dots N\right)=\left(1\dots N-1\right)\cup \left\{N\right\}$$
335	334	difeq1d	$$⊢\phi \to \left(1\dots N\right)\setminus \left\{N\right\}=\left(\left(1\dots N-1\right)\cup \left\{N\right\}\right)\setminus \left\{N\right\}$$
336		difun2	$$⊢\left(\left(1\dots N-1\right)\cup \left\{N\right\}\right)\setminus \left\{N\right\}=\left(1\dots N-1\right)\setminus \left\{N\right\}$$
337	335 336	eqtrdi	$$⊢\phi \to \left(1\dots N\right)\setminus \left\{N\right\}=\left(1\dots N-1\right)\setminus \left\{N\right\}$$
338		difsn	$$⊢\neg N\in \left(1\dots N-1\right)\to \left(1\dots N-1\right)\setminus \left\{N\right\}=\left(1\dots N-1\right)$$
339	164 338	syl	$$⊢\phi \to \left(1\dots N-1\right)\setminus \left\{N\right\}=\left(1\dots N-1\right)$$
340	337 339	eqtrd	$$⊢\phi \to \left(1\dots N\right)\setminus \left\{N\right\}=\left(1\dots N-1\right)$$
341	340	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(1\dots N\right)\setminus \left\{N\right\}=\left(1\dots N-1\right)$$
342	73	adantl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to N-1\in {\mathbb{Z}}_{\ge y}$$
343		fzsplit2	$$⊢\left(y+1\in {\mathbb{Z}}_{\ge 1}\wedge N-1\in {\mathbb{Z}}_{\ge y}\right)\to \left(1\dots N-1\right)=\left(1\dots y\right)\cup \left(y+1\dots N-1\right)$$
344	68 342 343	syl2anc	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(1\dots N-1\right)=\left(1\dots y\right)\cup \left(y+1\dots N-1\right)$$
345	341 344	eqtrd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(1\dots N\right)\setminus \left\{N\right\}=\left(1\dots y\right)\cup \left(y+1\dots N-1\right)$$
346	345	imaeq2d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\setminus \left\{N\right\}\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\cup \left(y+1\dots N-1\right)\right]$$
347		imadif	$$⊢\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 N\right)\setminus \left\{N\right\}\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\setminus 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left\{N\right\}\right]$$
348	49 347	syl	$$⊢\phi \to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\setminus \left\{N\right\}\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\setminus 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left\{N\right\}\right]$$
349		elfz1end	$$⊢N\in \mathbb{N}\leftrightarrow N\in \left(1\dots N\right)$$
350	1 349	sylib	$$⊢\phi \to N\in \left(1\dots N\right)$$
351		fnsnfv	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)Fn\left(1\dots N\right)\wedge N\in \left(1\dots N\right)\right)\to \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left\{N\right\}\right]$$
352	255 350 351	syl2anc	$$⊢\phi \to \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left\{N\right\}\right]$$
353	352	eqcomd	$$⊢\phi \to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left\{N\right\}\right]=\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}$$
354	83 353	difeq12d	$$⊢\phi \to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\setminus 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left\{N\right\}\right]=\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}$$
355	348 354	eqtrd	$$⊢\phi \to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\setminus \left\{N\right\}\right]=\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}$$
356	355	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\setminus \left\{N\right\}\right]=\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}$$
357	346 356	eqtr3d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\cup \left(y+1\dots N-1\right)\right]=\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}$$
358	333 357	eqtr3id	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cup 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]=\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}$$
359	358	fneq2d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)Fn\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cup 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\right)\leftrightarrow \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)Fn\left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\right)$$
360	332 359	mpbid	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)Fn\left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)$$
361		disjdifr	$$⊢\left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\cap \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}=\varnothing$$
362		fnconstg	$$⊢1\in \mathrm{V}\to \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)Fn\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}$$
363	34 362	ax-mp	$$⊢\left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)Fn\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}$$
364		fvun1	$$⊢\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)Fn\left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\wedge \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)Fn\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\wedge \left(\left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\cap \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}=\varnothing \wedge n\in \left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)\right)\left(n\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)$$
365	363 364	mp3an2	$$⊢\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)Fn\left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\wedge \left(\left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\cap \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}=\varnothing \wedge n\in \left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)\right)\left(n\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)$$
366		fnconstg	$$⊢0\in \mathrm{V}\to \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)Fn\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}$$
367	37 366	ax-mp	$$⊢\left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)Fn\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}$$
368		fvun1	$$⊢\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)Fn\left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\wedge \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)Fn\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\wedge \left(\left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\cap \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}=\varnothing \wedge n\in \left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)\right)\left(n\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)$$
369	367 368	mp3an2	$$⊢\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)Fn\left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\wedge \left(\left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\cap \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}=\varnothing \wedge n\in \left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)\right)\left(n\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)$$
370	365 369	eqtr4d	$$⊢\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)Fn\left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\wedge \left(\left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\cap \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}=\varnothing \wedge n\in \left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)\right)\left(n\right)=\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)\right)\left(n\right)$$
371	361 370	mpanr1	$$⊢\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)Fn\left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\wedge n\in \left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)\right)\left(n\right)=\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)\right)\left(n\right)$$
372	360 371	sylan	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(\left(1\dots N\right)\setminus \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)\right)\left(n\right)=\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)\right)\left(n\right)$$
373	320 372	sylan2br	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge \left(n\in \left(1\dots N\right)\wedge \neg n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)\right)\left(n\right)=\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)\right)\left(n\right)$$
374	373	anassrs	$$⊢\left(\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\wedge \neg n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)\right)\left(n\right)=\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)\right)\left(n\right)$$
375		imaundi	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1+1\dots y+1\right)\cup \left\{1\right\}\right]=\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1+1\dots y+1\right)\right]\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left\{1\right\}\right]$$
376		imaco	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1+1\dots y+1\right)\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1+1\dots y+1\right)\right]\right]$$
377		imaco	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left\{1\right\}\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left\{1\right\}\right]\right]$$
378	376 377	uneq12i	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1+1\dots y+1\right)\right]\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left\{1\right\}\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1+1\dots y+1\right)\right]\right]\cup 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left\{1\right\}\right]\right]$$
379	375 378	eqtri	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1+1\dots y+1\right)\cup \left\{1\right\}\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1+1\dots y+1\right)\right]\right]\cup 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left\{1\right\}\right]\right]$$
380		fzpred	$$⊢y+1\in {\mathbb{Z}}_{\ge 1}\to \left(1\dots y+1\right)=\left\{1\right\}\cup \left(1+1\dots y+1\right)$$
381	67 380	syl	$$⊢y\in \left(0\dots N-1\right)\to \left(1\dots y+1\right)=\left\{1\right\}\cup \left(1+1\dots y+1\right)$$
382		uncom	$$⊢\left\{1\right\}\cup \left(1+1\dots y+1\right)=\left(1+1\dots y+1\right)\cup \left\{1\right\}$$
383	381 382	eqtrdi	$$⊢y\in \left(0\dots N-1\right)\to \left(1\dots y+1\right)=\left(1+1\dots y+1\right)\cup \left\{1\right\}$$
384	383	imaeq2d	$$⊢y\in \left(0\dots N-1\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]=\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1+1\dots y+1\right)\cup \left\{1\right\}\right]$$
385	384	adantl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]=\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1+1\dots y+1\right)\cup \left\{1\right\}\right]$$
386		elfzelz	$$⊢y\in \left(0\dots N-1\right)\to y\in \mathbb{Z}$$
387	124	a1i	$$⊢y\in \mathbb{Z}\to 1+1-1=1$$
388		zcn	$$⊢y\in \mathbb{Z}\to y\in ℂ$$
389		pncan1	$$⊢y\in ℂ\to y+1-1=y$$
390	388 389	syl	$$⊢y\in \mathbb{Z}\to y+1-1=y$$
391	387 390	oveq12d	$$⊢y\in \mathbb{Z}\to \left(1+1-1\dots y+1-1\right)=\left(1\dots y\right)$$
392		elfzelz	$$⊢j\in \left(1+1-1\dots y+1-1\right)\to j\in \mathbb{Z}$$
393	392	zcnd	$$⊢j\in \left(1+1-1\dots y+1-1\right)\to j\in ℂ$$
394		pncan1	$$⊢j\in ℂ\to j+1-1=j$$
395	393 394	syl	$$⊢j\in \left(1+1-1\dots y+1-1\right)\to j+1-1=j$$
396	395	eleq1d	$$⊢j\in \left(1+1-1\dots y+1-1\right)\to \left(j+1-1\in \left(1+1-1\dots y+1-1\right)\leftrightarrow j\in \left(1+1-1\dots y+1-1\right)\right)$$
397	396	ibir	$$⊢j\in \left(1+1-1\dots y+1-1\right)\to j+1-1\in \left(1+1-1\dots y+1-1\right)$$
398	397	adantl	$$⊢\left(y\in \mathbb{Z}\wedge j\in \left(1+1-1\dots y+1-1\right)\right)\to j+1-1\in \left(1+1-1\dots y+1-1\right)$$
399		peano2z	$$⊢y\in \mathbb{Z}\to y+1\in \mathbb{Z}$$
400	399 117	jctil	$$⊢y\in \mathbb{Z}\to \left(1+1\in \mathbb{Z}\wedge y+1\in \mathbb{Z}\right)$$
401	392	peano2zd	$$⊢j\in \left(1+1-1\dots y+1-1\right)\to j+1\in \mathbb{Z}$$
402	401 115	jctir	$$⊢j\in \left(1+1-1\dots y+1-1\right)\to \left(j+1\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)$$
403		fzsubel	$$⊢\left(\left(1+1\in \mathbb{Z}\wedge y+1\in \mathbb{Z}\right)\wedge \left(j+1\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)\right)\to \left(j+1\in \left(1+1\dots y+1\right)\leftrightarrow j+1-1\in \left(1+1-1\dots y+1-1\right)\right)$$
404	400 402 403	syl2an	$$⊢\left(y\in \mathbb{Z}\wedge j\in \left(1+1-1\dots y+1-1\right)\right)\to \left(j+1\in \left(1+1\dots y+1\right)\leftrightarrow j+1-1\in \left(1+1-1\dots y+1-1\right)\right)$$
405	398 404	mpbird	$$⊢\left(y\in \mathbb{Z}\wedge j\in \left(1+1-1\dots y+1-1\right)\right)\to j+1\in \left(1+1\dots y+1\right)$$
406	395	eqcomd	$$⊢j\in \left(1+1-1\dots y+1-1\right)\to j=j+1-1$$
407	406	adantl	$$⊢\left(y\in \mathbb{Z}\wedge j\in \left(1+1-1\dots y+1-1\right)\right)\to j=j+1-1$$
408		oveq1	$$⊢n=j+1\to n-1=j+1-1$$
409	408	rspceeqv	$$⊢\left(j+1\in \left(1+1\dots y+1\right)\wedge j=j+1-1\right)\to \exists n\in \left(1+1\dots y+1\right)j=n-1$$
410	405 407 409	syl2anc	$$⊢\left(y\in \mathbb{Z}\wedge j\in \left(1+1-1\dots y+1-1\right)\right)\to \exists n\in \left(1+1\dots y+1\right)j=n-1$$
411	410	ex	$$⊢y\in \mathbb{Z}\to \left(j\in \left(1+1-1\dots y+1-1\right)\to \exists n\in \left(1+1\dots y+1\right)j=n-1\right)$$
412		simpr	$$⊢\left(y\in \mathbb{Z}\wedge n\in \left(1+1\dots y+1\right)\right)\to n\in \left(1+1\dots y+1\right)$$
413		elfzelz	$$⊢n\in \left(1+1\dots y+1\right)\to n\in \mathbb{Z}$$
414	413 115	jctir	$$⊢n\in \left(1+1\dots y+1\right)\to \left(n\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)$$
415		fzsubel	$$⊢\left(\left(1+1\in \mathbb{Z}\wedge y+1\in \mathbb{Z}\right)\wedge \left(n\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)\right)\to \left(n\in \left(1+1\dots y+1\right)\leftrightarrow n-1\in \left(1+1-1\dots y+1-1\right)\right)$$
416	400 414 415	syl2an	$$⊢\left(y\in \mathbb{Z}\wedge n\in \left(1+1\dots y+1\right)\right)\to \left(n\in \left(1+1\dots y+1\right)\leftrightarrow n-1\in \left(1+1-1\dots y+1-1\right)\right)$$
417	412 416	mpbid	$$⊢\left(y\in \mathbb{Z}\wedge n\in \left(1+1\dots y+1\right)\right)\to n-1\in \left(1+1-1\dots y+1-1\right)$$
418		eleq1	$$⊢j=n-1\to \left(j\in \left(1+1-1\dots y+1-1\right)\leftrightarrow n-1\in \left(1+1-1\dots y+1-1\right)\right)$$
419	417 418	syl5ibrcom	$$⊢\left(y\in \mathbb{Z}\wedge n\in \left(1+1\dots y+1\right)\right)\to \left(j=n-1\to j\in \left(1+1-1\dots y+1-1\right)\right)$$
420	419	rexlimdva	$$⊢y\in \mathbb{Z}\to \left(\exists n\in \left(1+1\dots y+1\right)j=n-1\to j\in \left(1+1-1\dots y+1-1\right)\right)$$
421	411 420	impbid	$$⊢y\in \mathbb{Z}\to \left(j\in \left(1+1-1\dots y+1-1\right)\leftrightarrow \exists n\in \left(1+1\dots y+1\right)j=n-1\right)$$
422		eqid	$$⊢\left(n\in \left(1+1\dots y+1\right)⟼n-1\right)=\left(n\in \left(1+1\dots y+1\right)⟼n-1\right)$$
423	422	elrnmpt	$$⊢j\in \mathrm{V}\to \left(j\in \mathrm{ran}\left(n\in \left(1+1\dots y+1\right)⟼n-1\right)\leftrightarrow \exists n\in \left(1+1\dots y+1\right)j=n-1\right)$$
424	423	elv	$$⊢j\in \mathrm{ran}\left(n\in \left(1+1\dots y+1\right)⟼n-1\right)\leftrightarrow \exists n\in \left(1+1\dots y+1\right)j=n-1$$
425	421 424	bitr4di	$$⊢y\in \mathbb{Z}\to \left(j\in \left(1+1-1\dots y+1-1\right)\leftrightarrow j\in \mathrm{ran}\left(n\in \left(1+1\dots y+1\right)⟼n-1\right)\right)$$
426	425	eqrdv	$$⊢y\in \mathbb{Z}\to \left(1+1-1\dots y+1-1\right)=\mathrm{ran}\left(n\in \left(1+1\dots y+1\right)⟼n-1\right)$$
427	391 426	eqtr3d	$$⊢y\in \mathbb{Z}\to \left(1\dots y\right)=\mathrm{ran}\left(n\in \left(1+1\dots y+1\right)⟼n-1\right)$$
428	386 427	syl	$$⊢y\in \left(0\dots N-1\right)\to \left(1\dots y\right)=\mathrm{ran}\left(n\in \left(1+1\dots y+1\right)⟼n-1\right)$$
429	428	adantl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(1\dots y\right)=\mathrm{ran}\left(n\in \left(1+1\dots y+1\right)⟼n-1\right)$$
430		df-ima	$$⊢\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1+1\dots y+1\right)\right]=\mathrm{ran}\left({\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\upharpoonright }_{\left(1+1\dots y+1\right)}\right)$$
431		uzid	$$⊢1\in \mathbb{Z}\to 1\in {\mathbb{Z}}_{\ge 1}$$
432		peano2uz	$$⊢1\in {\mathbb{Z}}_{\ge 1}\to 1+1\in {\mathbb{Z}}_{\ge 1}$$
433	115 431 432	mp2b	$$⊢1+1\in {\mathbb{Z}}_{\ge 1}$$
434		fzss1	$$⊢1+1\in {\mathbb{Z}}_{\ge 1}\to \left(1+1\dots y+1\right)\subseteq \left(1\dots y+1\right)$$
435	433 434	ax-mp	$$⊢\left(1+1\dots y+1\right)\subseteq \left(1\dots y+1\right)$$
436	435 272	sstrid	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(1+1\dots y+1\right)\subseteq \left(1\dots N\right)$$
437	436	resmptd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to {\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\upharpoonright }_{\left(1+1\dots y+1\right)}=\left(n\in \left(1+1\dots y+1\right)⟼if\left(n=1,N,n-1\right)\right)$$
438		elfzle1	$$⊢1\in \left(1+1\dots y+1\right)\to 1+1\le 1$$
439	171 438	mto	$$⊢\neg 1\in \left(1+1\dots y+1\right)$$
440		eleq1	$$⊢n=1\to \left(n\in \left(1+1\dots y+1\right)\leftrightarrow 1\in \left(1+1\dots y+1\right)\right)$$
441	439 440	mtbiri	$$⊢n=1\to \neg n\in \left(1+1\dots y+1\right)$$
442	441	necon2ai	$$⊢n\in \left(1+1\dots y+1\right)\to n\ne 1$$
443	442 182	syl	$$⊢n\in \left(1+1\dots y+1\right)\to if\left(n=1,N,n-1\right)=n-1$$
444	443	mpteq2ia	$$⊢\left(n\in \left(1+1\dots y+1\right)⟼if\left(n=1,N,n-1\right)\right)=\left(n\in \left(1+1\dots y+1\right)⟼n-1\right)$$
445	437 444	eqtrdi	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to {\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\upharpoonright }_{\left(1+1\dots y+1\right)}=\left(n\in \left(1+1\dots y+1\right)⟼n-1\right)$$
446	445	rneqd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \mathrm{ran}\left({\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\upharpoonright }_{\left(1+1\dots y+1\right)}\right)=\mathrm{ran}\left(n\in \left(1+1\dots y+1\right)⟼n-1\right)$$
447	430 446	eqtrid	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1+1\dots y+1\right)\right]=\mathrm{ran}\left(n\in \left(1+1\dots y+1\right)⟼n-1\right)$$
448	429 447	eqtr4d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(1\dots y\right)=\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1+1\dots y+1\right)\right]$$
449	448	imaeq2d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1+1\dots y+1\right)\right]\right]$$
450	266	sneqd	$$⊢\phi \to \left\{\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left(1\right)\right\}=\left\{N\right\}$$
451		fnsnfv	$$⊢\left(\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)Fn\left(1\dots N\right)\wedge 1\in \left(1\dots N\right)\right)\to \left\{\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left(1\right)\right\}=\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left\{1\right\}\right]$$
452	269 265 451	syl2anc	$$⊢\phi \to \left\{\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left(1\right)\right\}=\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left\{1\right\}\right]$$
453	450 452	eqtr3d	$$⊢\phi \to \left\{N\right\}=\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left\{1\right\}\right]$$
454	453	imaeq2d	$$⊢\phi \to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left\{N\right\}\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left\{1\right\}\right]\right]$$
455	352 454	eqtrd	$$⊢\phi \to \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left\{1\right\}\right]\right]$$
456	455	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left\{1\right\}\right]\right]$$
457	449 456	uneq12d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cup \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(1+1\dots y+1\right)\right]\right]\cup 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left\{1\right\}\right]\right]$$
458	379 385 457	3eqtr4a	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cup \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}$$
459	458	xpeq1d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}=\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cup \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\times \left\{1\right\}$$
460		xpundir	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\cup \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\times \left\{1\right\}=\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)$$
461	459 460	eqtrdi	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}=\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)$$
462		imaco	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(y+1+1\dots N\right)\right]\right]$$
463		df-ima	$$⊢\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(y+1+1\dots N\right)\right]=\mathrm{ran}\left({\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\upharpoonright }_{\left(y+1+1\dots N\right)}\right)$$
464		fzss1	$$⊢y+1+1\in {\mathbb{Z}}_{\ge 1}\to \left(y+1+1\dots N\right)\subseteq \left(1\dots N\right)$$
465	230 464	syl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(y+1+1\dots N\right)\subseteq \left(1\dots N\right)$$
466	465	resmptd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to {\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\upharpoonright }_{\left(y+1+1\dots N\right)}=\left(n\in \left(y+1+1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)$$
467		1red	$$⊢y\in \left(0\dots N-1\right)\to 1\in ℝ$$
468	65	nnzd	$$⊢y\in \left(0\dots N-1\right)\to y+1\in \mathbb{Z}$$
469	468	peano2zd	$$⊢y\in \left(0\dots N-1\right)\to y+1+1\in \mathbb{Z}$$
470	469	zred	$$⊢y\in \left(0\dots N-1\right)\to y+1+1\in ℝ$$
471	65	nnge1d	$$⊢y\in \left(0\dots N-1\right)\to 1\le y+1$$
472	467 217 470 471 218	lelttrd	$$⊢y\in \left(0\dots N-1\right)\to 1<y+1+1$$
473	467 470	ltnled	$$⊢y\in \left(0\dots N-1\right)\to \left(1<y+1+1\leftrightarrow \neg y+1+1\le 1\right)$$
474	472 473	mpbid	$$⊢y\in \left(0\dots N-1\right)\to \neg y+1+1\le 1$$
475		elfzle1	$$⊢1\in \left(y+1+1\dots N\right)\to y+1+1\le 1$$
476	474 475	nsyl	$$⊢y\in \left(0\dots N-1\right)\to \neg 1\in \left(y+1+1\dots N\right)$$
477		eleq1	$$⊢n=1\to \left(n\in \left(y+1+1\dots N\right)\leftrightarrow 1\in \left(y+1+1\dots N\right)\right)$$
478	477	notbid	$$⊢n=1\to \left(\neg n\in \left(y+1+1\dots N\right)\leftrightarrow \neg 1\in \left(y+1+1\dots N\right)\right)$$
479	476 478	syl5ibrcom	$$⊢y\in \left(0\dots N-1\right)\to \left(n=1\to \neg n\in \left(y+1+1\dots N\right)\right)$$
480	479	necon2ad	$$⊢y\in \left(0\dots N-1\right)\to \left(n\in \left(y+1+1\dots N\right)\to n\ne 1\right)$$
481	480	imp	$$⊢\left(y\in \left(0\dots N-1\right)\wedge n\in \left(y+1+1\dots N\right)\right)\to n\ne 1$$
482	481 182	syl	$$⊢\left(y\in \left(0\dots N-1\right)\wedge n\in \left(y+1+1\dots N\right)\right)\to if\left(n=1,N,n-1\right)=n-1$$
483	482	mpteq2dva	$$⊢y\in \left(0\dots N-1\right)\to \left(n\in \left(y+1+1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)=\left(n\in \left(y+1+1\dots N\right)⟼n-1\right)$$
484	483	adantl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(n\in \left(y+1+1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)=\left(n\in \left(y+1+1\dots N\right)⟼n-1\right)$$
485	466 484	eqtrd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to {\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\upharpoonright }_{\left(y+1+1\dots N\right)}=\left(n\in \left(y+1+1\dots N\right)⟼n-1\right)$$
486	485	rneqd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \mathrm{ran}\left({\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\upharpoonright }_{\left(y+1+1\dots N\right)}\right)=\mathrm{ran}\left(n\in \left(y+1+1\dots N\right)⟼n-1\right)$$
487	463 486	eqtrid	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(y+1+1\dots N\right)\right]=\mathrm{ran}\left(n\in \left(y+1+1\dots N\right)⟼n-1\right)$$
488		eqid	$$⊢\left(n\in \left(y+1+1\dots N\right)⟼n-1\right)=\left(n\in \left(y+1+1\dots N\right)⟼n-1\right)$$
489	488	elrnmpt	$$⊢j\in \mathrm{V}\to \left(j\in \mathrm{ran}\left(n\in \left(y+1+1\dots N\right)⟼n-1\right)\leftrightarrow \exists n\in \left(y+1+1\dots N\right)j=n-1\right)$$
490	489	elv	$$⊢j\in \mathrm{ran}\left(n\in \left(y+1+1\dots N\right)⟼n-1\right)\leftrightarrow \exists n\in \left(y+1+1\dots N\right)j=n-1$$
491		simpr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(y+1+1\dots N\right)\right)\to n\in \left(y+1+1\dots N\right)$$
492	114 469	anim12ci	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(y+1+1\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)$$
493		elfzelz	$$⊢n\in \left(y+1+1\dots N\right)\to n\in \mathbb{Z}$$
494	493 115	jctir	$$⊢n\in \left(y+1+1\dots N\right)\to \left(n\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)$$
495		fzsubel	$$⊢\left(\left(y+1+1\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\wedge \left(n\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)\right)\to \left(n\in \left(y+1+1\dots N\right)\leftrightarrow n-1\in \left(\left(y+1\right)+1-1\dots N-1\right)\right)$$
496	492 494 495	syl2an	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(y+1+1\dots N\right)\right)\to \left(n\in \left(y+1+1\dots N\right)\leftrightarrow n-1\in \left(\left(y+1\right)+1-1\dots N-1\right)\right)$$
497	491 496	mpbid	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(y+1+1\dots N\right)\right)\to n-1\in \left(\left(y+1\right)+1-1\dots N-1\right)$$
498		eleq1	$$⊢j=n-1\to \left(j\in \left(\left(y+1\right)+1-1\dots N-1\right)\leftrightarrow n-1\in \left(\left(y+1\right)+1-1\dots N-1\right)\right)$$
499	497 498	syl5ibrcom	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(y+1+1\dots N\right)\right)\to \left(j=n-1\to j\in \left(\left(y+1\right)+1-1\dots N-1\right)\right)$$
500	499	rexlimdva	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\exists n\in \left(y+1+1\dots N\right)j=n-1\to j\in \left(\left(y+1\right)+1-1\dots N-1\right)\right)$$
501		elfzelz	$$⊢j\in \left(\left(y+1\right)+1-1\dots N-1\right)\to j\in \mathbb{Z}$$
502	501	zcnd	$$⊢j\in \left(\left(y+1\right)+1-1\dots N-1\right)\to j\in ℂ$$
503	502 394	syl	$$⊢j\in \left(\left(y+1\right)+1-1\dots N-1\right)\to j+1-1=j$$
504	503	eleq1d	$$⊢j\in \left(\left(y+1\right)+1-1\dots N-1\right)\to \left(j+1-1\in \left(\left(y+1\right)+1-1\dots N-1\right)\leftrightarrow j\in \left(\left(y+1\right)+1-1\dots N-1\right)\right)$$
505	504	ibir	$$⊢j\in \left(\left(y+1\right)+1-1\dots N-1\right)\to j+1-1\in \left(\left(y+1\right)+1-1\dots N-1\right)$$
506	505	adantl	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge j\in \left(\left(y+1\right)+1-1\dots N-1\right)\right)\to j+1-1\in \left(\left(y+1\right)+1-1\dots N-1\right)$$
507	501	peano2zd	$$⊢j\in \left(\left(y+1\right)+1-1\dots N-1\right)\to j+1\in \mathbb{Z}$$
508	507 115	jctir	$$⊢j\in \left(\left(y+1\right)+1-1\dots N-1\right)\to \left(j+1\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)$$
509		fzsubel	$$⊢\left(\left(y+1+1\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\wedge \left(j+1\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)\right)\to \left(j+1\in \left(y+1+1\dots N\right)\leftrightarrow j+1-1\in \left(\left(y+1\right)+1-1\dots N-1\right)\right)$$
510	492 508 509	syl2an	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge j\in \left(\left(y+1\right)+1-1\dots N-1\right)\right)\to \left(j+1\in \left(y+1+1\dots N\right)\leftrightarrow j+1-1\in \left(\left(y+1\right)+1-1\dots N-1\right)\right)$$
511	506 510	mpbird	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge j\in \left(\left(y+1\right)+1-1\dots N-1\right)\right)\to j+1\in \left(y+1+1\dots N\right)$$
512	503	eqcomd	$$⊢j\in \left(\left(y+1\right)+1-1\dots N-1\right)\to j=j+1-1$$
513	512	adantl	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge j\in \left(\left(y+1\right)+1-1\dots N-1\right)\right)\to j=j+1-1$$
514	408	rspceeqv	$$⊢\left(j+1\in \left(y+1+1\dots N\right)\wedge j=j+1-1\right)\to \exists n\in \left(y+1+1\dots N\right)j=n-1$$
515	511 513 514	syl2anc	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge j\in \left(\left(y+1\right)+1-1\dots N-1\right)\right)\to \exists n\in \left(y+1+1\dots N\right)j=n-1$$
516	515	ex	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(j\in \left(\left(y+1\right)+1-1\dots N-1\right)\to \exists n\in \left(y+1+1\dots N\right)j=n-1\right)$$
517	500 516	impbid	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\exists n\in \left(y+1+1\dots N\right)j=n-1\leftrightarrow j\in \left(\left(y+1\right)+1-1\dots N-1\right)\right)$$
518	490 517	bitrid	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(j\in \mathrm{ran}\left(n\in \left(y+1+1\dots N\right)⟼n-1\right)\leftrightarrow j\in \left(\left(y+1\right)+1-1\dots N-1\right)\right)$$
519	518	eqrdv	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \mathrm{ran}\left(n\in \left(y+1+1\dots N\right)⟼n-1\right)=\left(\left(y+1\right)+1-1\dots N-1\right)$$
520	65	nncnd	$$⊢y\in \left(0\dots N-1\right)\to y+1\in ℂ$$
521		pncan1	$$⊢y+1\in ℂ\to \left(y+1\right)+1-1=y+1$$
522	520 521	syl	$$⊢y\in \left(0\dots N-1\right)\to \left(y+1\right)+1-1=y+1$$
523	522	oveq1d	$$⊢y\in \left(0\dots N-1\right)\to \left(\left(y+1\right)+1-1\dots N-1\right)=\left(y+1\dots N-1\right)$$
524	523	adantl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(y+1\right)+1-1\dots N-1\right)=\left(y+1\dots N-1\right)$$
525	487 519 524	3eqtrd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(y+1+1\dots N\right)\right]=\left(y+1\dots N-1\right)$$
526	525	imaeq2d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\left[\left(y+1+1\dots N\right)\right]\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]$$
527	462 526	eqtrid	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]$$
528	527	xpeq1d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}$$
529	461 528	uneq12d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)$$
530		un23	$$⊢\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)$$
531	529 530	eqtrdi	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)$$
532	531	fveq1d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)=\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)\right)\left(n\right)$$
533	532	ad2antrr	$$⊢\left(\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\wedge \neg n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)=\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{1\right\}\right)\right)\left(n\right)$$
534		imaundi	$$⊢2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\cup \left\{N\right\}\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\cup 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left\{N\right\}\right]$$
535		fzsplit2	$$⊢\left(N-1+1\in {\mathbb{Z}}_{\ge \left(y+1\right)}\wedge N\in {\mathbb{Z}}_{\ge \left(N-1\right)}\right)\to \left(y+1\dots N\right)=\left(y+1\dots N-1\right)\cup \left(N-1+1\dots N\right)$$
536	232 200 535	syl2anr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(y+1\dots N\right)=\left(y+1\dots N-1\right)\cup \left(N-1+1\dots N\right)$$
537	206	uneq2d	$$⊢\phi \to \left(y+1\dots N-1\right)\cup \left(N-1+1\dots N\right)=\left(y+1\dots N-1\right)\cup \left\{N\right\}$$
538	537	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(y+1\dots N-1\right)\cup \left(N-1+1\dots N\right)=\left(y+1\dots N-1\right)\cup \left\{N\right\}$$
539	536 538	eqtrd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(y+1\dots N\right)=\left(y+1\dots N-1\right)\cup \left\{N\right\}$$
540	539	imaeq2d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\cup \left\{N\right\}\right]$$
541	352	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left\{N\right\}\right]$$
542	541	uneq2d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\cup \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\cup 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left\{N\right\}\right]$$
543	534 540 542	3eqtr4a	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\cup \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}$$
544	543	xpeq1d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}=\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\cup \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\times \left\{0\right\}$$
545		xpundir	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\cup \left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\right)\times \left\{0\right\}=\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)$$
546	544 545	eqtrdi	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}=\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)$$
547	546	uneq2d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)=\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)\right)$$
548		unass	$$⊢\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)=\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)\right)$$
549	547 548	eqtr4di	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)$$
550	549	fveq1d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)=\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)\right)\left(n\right)$$
551	550	ad2antrr	$$⊢\left(\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\wedge \neg n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)=\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N-1\right)\right]\times \left\{0\right\}\right)\right)\cup \left(\left\{2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right\}\times \left\{0\right\}\right)\right)\left(n\right)$$
552	374 533 551	3eqtr4d	$$⊢\left(\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\wedge \neg n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)$$
553	316 552	eqtrd	$$⊢\left(\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\wedge \neg n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-0=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)$$
554	250 252 314 553	ifbothda	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)=\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)$$
555	554	oveq2d	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\to 1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)+\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)=1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)+\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)$$
556	248 555	eqtr2d	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\to 1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)+\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)=1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)+\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)$$
557	556	mpteq2dva	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(n\in \left(1\dots N\right)⟼1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)+\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)\right)=\left(n\in \left(1\dots N\right)⟼1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)+\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)\right)$$
558	93 557	eqtrd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\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 y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)=\left(n\in \left(1\dots N\right)⟼1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)+\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)\right)$$
559	53	adantl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to y\in ℝ$$
560	160	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to N-1\in ℝ$$
561	158	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to N\in ℝ$$
562		elfzle2	$$⊢y\in \left(0\dots N-1\right)\to y\le N-1$$
563	562	adantl	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to y\le N-1$$
564	159	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to N-1<N$$
565	559 560 561 563 564	lelttrd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to y<N$$
566	6	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to 2^{nd}\left(T\right)=N$$
567	565 566	breqtrrd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to y<2^{nd}\left(T\right)$$
568	567	iftrued	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to if\left(y<2^{nd}\left(T\right),y,y+1\right)=y$$
569	568	csbeq1d	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to ⦋if\left(y<2^{nd}\left(T\right),y,y+1\right)/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)=⦋y/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)$$
570		vex	$$⊢y\in \mathrm{V}$$
571		oveq2	$$⊢j=y\to \left(1\dots j\right)=\left(1\dots y\right)$$
572	571	imaeq2d	$$⊢j=y\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 y\right)\right]$$
573	572	xpeq1d	$$⊢j=y\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots j\right)\right]\times \left\{1\right\}=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}$$
574		oveq1	$$⊢j=y\to j+1=y+1$$
575	574	oveq1d	$$⊢j=y\to \left(j+1\dots N\right)=\left(y+1\dots N\right)$$
576	575	imaeq2d	$$⊢j=y\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(y+1\dots N\right)\right]$$
577	576	xpeq1d	$$⊢j=y\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}$$
578	573 577	uneq12d	$$⊢j=y\to \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)=\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)$$
579	578	oveq2d	$$⊢j=y\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]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \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 y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)$$
580	570 579	csbie	$$⊢⦋y/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\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 y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)$$
581	569 580	eqtrdi	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to ⦋if\left(y<2^{nd}\left(T\right),y,y+1\right)/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\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 y\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(y+1\dots N\right)\right]\times \left\{0\right\}\right)\right)$$
582		ovexd	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\to 1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)\in \mathrm{V}$$
583		fvexd	$$⊢\left(\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\wedge n\in \left(1\dots N\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)\in \mathrm{V}$$
584		eqidd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(n\in \left(1\dots N\right)⟼1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)\right)=\left(n\in \left(1\dots N\right)⟼1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)\right)$$
585	245	ffnd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)Fn\left(1\dots N\right)$$
586		nfcv	$$⊢\underset{\_}{Ⅎ}n{2}^{nd}\left(1^{st}\left(T\right)\right)$$
587		nfmpt1	$$⊢\underset{\_}{Ⅎ}n\left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)$$
588	586 587	nfco	$$⊢\underset{\_}{Ⅎ}n\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)$$
589		nfcv	$$⊢\underset{\_}{Ⅎ}n\left(1\dots y+1\right)$$
590	588 589	nfima	$$⊢\underset{\_}{Ⅎ}n\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]$$
591		nfcv	$$⊢\underset{\_}{Ⅎ}n\left\{1\right\}$$
592	590 591	nfxp	$$⊢\underset{\_}{Ⅎ}n\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)$$
593		nfcv	$$⊢\underset{\_}{Ⅎ}n\left(y+1+1\dots N\right)$$
594	588 593	nfima	$$⊢\underset{\_}{Ⅎ}n\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]$$
595		nfcv	$$⊢\underset{\_}{Ⅎ}n\left\{0\right\}$$
596	594 595	nfxp	$$⊢\underset{\_}{Ⅎ}n\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)$$
597	592 596	nfun	$$⊢\underset{\_}{Ⅎ}n\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)$$
598	597	dffn5f	$$⊢\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)Fn\left(1\dots N\right)\leftrightarrow \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)=\left(n\in \left(1\dots N\right)⟼\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)\right)$$
599	585 598	sylib	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)=\left(n\in \left(1\dots N\right)⟼\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)\right)$$
600	89 582 583 584 599	offval2	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(n\in \left(1\dots N\right)⟼1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)\right){+}_f\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)=\left(n\in \left(1\dots N\right)⟼1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)+\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\left(n\right)\right)$$
601	558 581 600	3eqtr4rd	$$⊢\left(\phi \wedge y\in \left(0\dots N-1\right)\right)\to \left(n\in \left(1\dots N\right)⟼1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)\right){+}_f\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)=⦋if\left(y<2^{nd}\left(T\right),y,y+1\right)/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)$$
602	601	mpteq2dva	$$⊢\phi \to \left(y\in \left(0\dots N-1\right)⟼\left(n\in \left(1\dots N\right)⟼1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)\right){+}_f\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)=\left(y\in \left(0\dots N-1\right)⟼⦋if\left(y<2^{nd}\left(T\right),y,y+1\right)/j⦌\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 j\right)\right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)\right)$$
603	23 602	eqtr4d	$$⊢\phi \to F=\left(y\in \left(0\dots N-1\right)⟼\left(n\in \left(1\dots N\right)⟼1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)-if\left(n=2^{nd}\left(1^{st}\left(T\right)\right)\left(N\right),1,0\right)\right){+}_f\left(\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(1\dots y+1\right)\right]\times \left\{1\right\}\right)\cup \left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\circ \left(n\in \left(1\dots N\right)⟼if\left(n=1,N,n-1\right)\right)\right)\left[\left(y+1+1\dots N\right)\right]\times \left\{0\right\}\right)\right)\right)$$