Theorem poimirlem10

Description: Lemma for poimir establishing the cube that yields the simplex that yields a face if the opposite vertex was first on the walk. (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)}$$
	poimirlem12.2	$$⊢\phi \to T\in S$$
	poimirlem11.3	$$⊢\phi \to 2^{nd}\left(T\right)=0$$
Assertion	poimirlem10	$$⊢\phi \to F\left(N-1\right){-}_f\left(\left(1\dots N\right)\times \left\{1\right\}\right)=1^{st}\left(1^{st}\left(T\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		poimirlem12.2	$$⊢\phi \to T\in S$$
5		poimirlem11.3	$$⊢\phi \to 2^{nd}\left(T\right)=0$$
6		ovexd	$$⊢\phi \to \left(1\dots N\right)\in \mathrm{V}$$
7		nnm1nn0	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{N}}_0$$
8	1 7	syl	$$⊢\phi \to N-1\in {\mathbb{N}}_0$$
9		nn0fz0	$$⊢N-1\in {\mathbb{N}}_0\leftrightarrow N-1\in \left(0\dots N-1\right)$$
10	8 9	sylib	$$⊢\phi \to N-1\in \left(0\dots N-1\right)$$
11	3 10	ffvelcdmd	$$⊢\phi \to F\left(N-1\right)\in \left({\left(0\dots K\right)}^{\left(1\dots N\right)}\right)$$
12		elmapfn	$$⊢F\left(N-1\right)\in \left({\left(0\dots K\right)}^{\left(1\dots N\right)}\right)\to F\left(N-1\right)Fn\left(1\dots N\right)$$
13	11 12	syl	$$⊢\phi \to F\left(N-1\right)Fn\left(1\dots N\right)$$
14		1ex	$$⊢1\in \mathrm{V}$$
15		fnconstg	$$⊢1\in \mathrm{V}\to \left(\left(1\dots N\right)\times \left\{1\right\}\right)Fn\left(1\dots N\right)$$
16	14 15	mp1i	$$⊢\phi \to \left(\left(1\dots N\right)\times \left\{1\right\}\right)Fn\left(1\dots N\right)$$
17		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)$$
18	17 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)$$
19	4 18	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)$$
20		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)$$
21	19 20	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)$$
22		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)$$
23	21 22	syl	$$⊢\phi \to 1^{st}\left(1^{st}\left(T\right)\right)\in \left({\left(0..^K\right)}^{\left(1\dots N\right)}\right)$$
24		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)$$
25	23 24	syl	$$⊢\phi \to 1^{st}\left(1^{st}\left(T\right)\right)Fn\left(1\dots N\right)$$
26		fveq2	$$⊢t=T\to 2^{nd}\left(t\right)=2^{nd}\left(T\right)$$
27	26	breq2d	$$⊢t=T\to \left(y<2^{nd}\left(t\right)\leftrightarrow y<2^{nd}\left(T\right)\right)$$
28	27	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)$$
29	28	csbeq1d	$$⊢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)$$
30		2fveq3	$$⊢t=T\to 1^{st}\left(1^{st}\left(t\right)\right)=1^{st}\left(1^{st}\left(T\right)\right)$$
31		2fveq3	$$⊢t=T\to 2^{nd}\left(1^{st}\left(t\right)\right)=2^{nd}\left(1^{st}\left(T\right)\right)$$
32	31	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]$$
33	32	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\}$$
34	31	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]$$
35	34	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\}$$
36	33 35	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)$$
37	30 36	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)$$
38	37	csbeq2dv	$$⊢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)$$
39	29 38	eqtrd	$$⊢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)$$
40	39	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)$$
41	40	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)$$
42	41 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)$$
43	42	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)$$
44	4 43	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)$$
45		breq12	$$⊢\left(y=N-1\wedge 2^{nd}\left(T\right)=0\right)\to \left(y<2^{nd}\left(T\right)\leftrightarrow N-1<0\right)$$
46	5 45	sylan2	$$⊢\left(y=N-1\wedge \phi \right)\to \left(y<2^{nd}\left(T\right)\leftrightarrow N-1<0\right)$$
47	46	ancoms	$$⊢\left(\phi \wedge y=N-1\right)\to \left(y<2^{nd}\left(T\right)\leftrightarrow N-1<0\right)$$
48		oveq1	$$⊢y=N-1\to y+1=N-1+1$$
49	1	nncnd	$$⊢\phi \to N\in ℂ$$
50		npcan1	$$⊢N\in ℂ\to N-1+1=N$$
51	49 50	syl	$$⊢\phi \to N-1+1=N$$
52	48 51	sylan9eqr	$$⊢\left(\phi \wedge y=N-1\right)\to y+1=N$$
53	47 52	ifbieq2d	$$⊢\left(\phi \wedge y=N-1\right)\to if\left(y<2^{nd}\left(T\right),y,y+1\right)=if\left(N-1<0,y,N\right)$$
54	8	nn0ge0d	$$⊢\phi \to 0\le N-1$$
55		0red	$$⊢\phi \to 0\in ℝ$$
56	8	nn0red	$$⊢\phi \to N-1\in ℝ$$
57	55 56	lenltd	$$⊢\phi \to \left(0\le N-1\leftrightarrow \neg N-1<0\right)$$
58	54 57	mpbid	$$⊢\phi \to \neg N-1<0$$
59	58	iffalsed	$$⊢\phi \to if\left(N-1<0,y,N\right)=N$$
60	59	adantr	$$⊢\left(\phi \wedge y=N-1\right)\to if\left(N-1<0,y,N\right)=N$$
61	53 60	eqtrd	$$⊢\left(\phi \wedge y=N-1\right)\to if\left(y<2^{nd}\left(T\right),y,y+1\right)=N$$
62	61	csbeq1d	$$⊢\left(\phi \wedge y=N-1\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)=⦋N/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)$$
63		oveq2	$$⊢j=N\to \left(1\dots j\right)=\left(1\dots N\right)$$
64	63	imaeq2d	$$⊢j=N\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 N\right)\right]$$
65		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\}$$
66	21 65	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\}$$
67		fvex	$$⊢2^{nd}\left(1^{st}\left(T\right)\right)\in \mathrm{V}$$
68		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)$$
69	67 68	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)$$
70	66 69	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)$$
71		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)$$
72		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)$$
73	70 71 72	3syl	$$⊢\phi \to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]=\left(1\dots N\right)$$
74	64 73	sylan9eqr	$$⊢\left(\phi \wedge j=N\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots j\right)\right]=\left(1\dots N\right)$$
75	74	xpeq1d	$$⊢\left(\phi \wedge j=N\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots j\right)\right]\times \left\{1\right\}=\left(1\dots N\right)\times \left\{1\right\}$$
76		oveq1	$$⊢j=N\to j+1=N+1$$
77	76	oveq1d	$$⊢j=N\to \left(j+1\dots N\right)=\left(N+1\dots N\right)$$
78	1	nnred	$$⊢\phi \to N\in ℝ$$
79	78	ltp1d	$$⊢\phi \to N<N+1$$
80	1	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
81	80	peano2zd	$$⊢\phi \to N+1\in \mathbb{Z}$$
82		fzn	$$⊢\left(N+1\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(N<N+1\leftrightarrow \left(N+1\dots N\right)=\varnothing \right)$$
83	81 80 82	syl2anc	$$⊢\phi \to \left(N<N+1\leftrightarrow \left(N+1\dots N\right)=\varnothing \right)$$
84	79 83	mpbid	$$⊢\phi \to \left(N+1\dots N\right)=\varnothing$$
85	77 84	sylan9eqr	$$⊢\left(\phi \wedge j=N\right)\to \left(j+1\dots N\right)=\varnothing$$
86	85	imaeq2d	$$⊢\left(\phi \wedge j=N\right)\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[\varnothing \right]$$
87	86	xpeq1d	$$⊢\left(\phi \wedge j=N\right)\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[\varnothing \right]\times \left\{0\right\}$$
88		ima0	$$⊢2^{nd}\left(1^{st}\left(T\right)\right)\left[\varnothing \right]=\varnothing$$
89	88	xpeq1i	$$⊢2^{nd}\left(1^{st}\left(T\right)\right)\left[\varnothing \right]\times \left\{0\right\}=\varnothing \times \left\{0\right\}$$
90		0xp	$$⊢\varnothing \times \left\{0\right\}=\varnothing$$
91	89 90	eqtri	$$⊢2^{nd}\left(1^{st}\left(T\right)\right)\left[\varnothing \right]\times \left\{0\right\}=\varnothing$$
92	87 91	eqtrdi	$$⊢\left(\phi \wedge j=N\right)\to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(j+1\dots N\right)\right]\times \left\{0\right\}=\varnothing$$
93	75 92	uneq12d	$$⊢\left(\phi \wedge j=N\right)\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(\left(1\dots N\right)\times \left\{1\right\}\right)\cup \varnothing$$
94		un0	$$⊢\left(\left(1\dots N\right)\times \left\{1\right\}\right)\cup \varnothing =\left(1\dots N\right)\times \left\{1\right\}$$
95	93 94	eqtrdi	$$⊢\left(\phi \wedge j=N\right)\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(1\dots N\right)\times \left\{1\right\}$$
96	95	oveq2d	$$⊢\left(\phi \wedge j=N\right)\to 1^{st}\left(1^{st}\left(T\right)\right){+}_f\left(\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots j\right)\right]\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(1\dots N\right)\times \left\{1\right\}\right)$$
97	1 96	csbied	$$⊢\phi \to ⦋N/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(1\dots N\right)\times \left\{1\right\}\right)$$
98	97	adantr	$$⊢\left(\phi \wedge y=N-1\right)\to ⦋N/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(1\dots N\right)\times \left\{1\right\}\right)$$
99	62 98	eqtrd	$$⊢\left(\phi \wedge y=N-1\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(1\dots N\right)\times \left\{1\right\}\right)$$
100		ovexd	$$⊢\phi \to 1^{st}\left(1^{st}\left(T\right)\right){+}_f\left(\left(1\dots N\right)\times \left\{1\right\}\right)\in \mathrm{V}$$
101	44 99 10 100	fvmptd	$$⊢\phi \to F\left(N-1\right)=1^{st}\left(1^{st}\left(T\right)\right){+}_f\left(\left(1\dots N\right)\times \left\{1\right\}\right)$$
102	101	fveq1d	$$⊢\phi \to F\left(N-1\right)\left(n\right)=\left(1^{st}\left(1^{st}\left(T\right)\right){+}_f\left(\left(1\dots N\right)\times \left\{1\right\}\right)\right)\left(n\right)$$
103	102	adantr	$$⊢\left(\phi \wedge n\in \left(1\dots N\right)\right)\to F\left(N-1\right)\left(n\right)=\left(1^{st}\left(1^{st}\left(T\right)\right){+}_f\left(\left(1\dots N\right)\times \left\{1\right\}\right)\right)\left(n\right)$$
104		inidm	$$⊢\left(1\dots N\right)\cap \left(1\dots N\right)=\left(1\dots N\right)$$
105		eqidd	$$⊢\left(\phi \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)$$
106	14	fvconst2	$$⊢n\in \left(1\dots N\right)\to \left(\left(1\dots N\right)\times \left\{1\right\}\right)\left(n\right)=1$$
107	106	adantl	$$⊢\left(\phi \wedge n\in \left(1\dots N\right)\right)\to \left(\left(1\dots N\right)\times \left\{1\right\}\right)\left(n\right)=1$$
108	25 16 6 6 104 105 107	ofval	$$⊢\left(\phi \wedge n\in \left(1\dots N\right)\right)\to \left(1^{st}\left(1^{st}\left(T\right)\right){+}_f\left(\left(1\dots N\right)\times \left\{1\right\}\right)\right)\left(n\right)=1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)+1$$
109	103 108	eqtrd	$$⊢\left(\phi \wedge n\in \left(1\dots N\right)\right)\to F\left(N-1\right)\left(n\right)=1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)+1$$
110		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)$$
111	23 110	syl	$$⊢\phi \to 1^{st}\left(1^{st}\left(T\right)\right):\left(1\dots N\right)⟶\left(0..^K\right)$$
112	111	ffvelcdmda	$$⊢\left(\phi \wedge n\in \left(1\dots N\right)\right)\to 1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)\in \left(0..^K\right)$$
113		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$$
114	112 113	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$$
115	114	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 ℂ$$
116		pncan1	$$⊢1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)\in ℂ\to 1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)+1-1=1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)$$
117	115 116	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)+1-1=1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)$$
118	6 13 16 25 109 107 117	offveq	$$⊢\phi \to F\left(N-1\right){-}_f\left(\left(1\dots N\right)\times \left\{1\right\}\right)=1^{st}\left(1^{st}\left(T\right)\right)$$