Theorem poimirlem16

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