Theorem poimirlem5

Description: Lemma for poimir to establish that, for the simplices defined by a walk along the edges of an N -cube, if the starting vertex is not opposite a given face, it is the earliest vertex of the face 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\}$$
	poimirlem9.1	$$⊢\phi \to T\in S$$
	poimirlem5.2	$$⊢\phi \to 0<2^{nd}\left(T\right)$$
Assertion	poimirlem5	$$⊢\phi \to F\left(0\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		poimirlem9.1	$$⊢\phi \to T\in S$$
4		poimirlem5.2	$$⊢\phi \to 0<2^{nd}\left(T\right)$$
5		fveq2	$$⊢t=T\to 2^{nd}\left(t\right)=2^{nd}\left(T\right)$$
6	5	breq2d	$$⊢t=T\to \left(y<2^{nd}\left(t\right)\leftrightarrow y<2^{nd}\left(T\right)\right)$$
7	6	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)$$
8	7	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)$$
9		2fveq3	$$⊢t=T\to 1^{st}\left(1^{st}\left(t\right)\right)=1^{st}\left(1^{st}\left(T\right)\right)$$
10		2fveq3	$$⊢t=T\to 2^{nd}\left(1^{st}\left(t\right)\right)=2^{nd}\left(1^{st}\left(T\right)\right)$$
11	10	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]$$
12	11	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\}$$
13	10	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]$$
14	13	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\}$$
15	12 14	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)$$
16	9 15	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)$$
17	16	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)$$
18	8 17	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)$$
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	3 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		breq1	$$⊢y=0\to \left(y<2^{nd}\left(T\right)\leftrightarrow 0<2^{nd}\left(T\right)\right)$$
25		id	$$⊢y=0\to y=0$$
26	24 25	ifbieq1d	$$⊢y=0\to if\left(y<2^{nd}\left(T\right),y,y+1\right)=if\left(0<2^{nd}\left(T\right),0,y+1\right)$$
27	4	iftrued	$$⊢\phi \to if\left(0<2^{nd}\left(T\right),0,y+1\right)=0$$
28	26 27	sylan9eqr	$$⊢\left(\phi \wedge y=0\right)\to if\left(y<2^{nd}\left(T\right),y,y+1\right)=0$$
29	28	csbeq1d	$$⊢\left(\phi \wedge y=0\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)=⦋0/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		c0ex	$$⊢0\in \mathrm{V}$$
31		oveq2	$$⊢j=0\to \left(1\dots j\right)=\left(1\dots 0\right)$$
32		fz10	$$⊢\left(1\dots 0\right)=\varnothing$$
33	31 32	eqtrdi	$$⊢j=0\to \left(1\dots j\right)=\varnothing$$
34	33	imaeq2d	$$⊢j=0\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[\varnothing \right]$$
35	34	xpeq1d	$$⊢j=0\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[\varnothing \right]\times \left\{1\right\}$$
36		oveq1	$$⊢j=0\to j+1=0+1$$
37		0p1e1	$$⊢0+1=1$$
38	36 37	eqtrdi	$$⊢j=0\to j+1=1$$
39	38	oveq1d	$$⊢j=0\to \left(j+1\dots N\right)=\left(1\dots N\right)$$
40	39	imaeq2d	$$⊢j=0\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(1\dots N\right)\right]$$
41	40	xpeq1d	$$⊢j=0\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(1\dots N\right)\right]\times \left\{0\right\}$$
42	35 41	uneq12d	$$⊢j=0\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[\varnothing \right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\times \left\{0\right\}\right)$$
43		ima0	$$⊢2^{nd}\left(1^{st}\left(T\right)\right)\left[\varnothing \right]=\varnothing$$
44	43	xpeq1i	$$⊢2^{nd}\left(1^{st}\left(T\right)\right)\left[\varnothing \right]\times \left\{1\right\}=\varnothing \times \left\{1\right\}$$
45		0xp	$$⊢\varnothing \times \left\{1\right\}=\varnothing$$
46	44 45	eqtri	$$⊢2^{nd}\left(1^{st}\left(T\right)\right)\left[\varnothing \right]\times \left\{1\right\}=\varnothing$$
47	46	uneq1i	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\varnothing \right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\times \left\{0\right\}\right)=\varnothing \cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\times \left\{0\right\}\right)$$
48		uncom	$$⊢\varnothing \cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\times \left\{0\right\}\right)=\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\times \left\{0\right\}\right)\cup \varnothing$$
49		un0	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\times \left\{0\right\}\right)\cup \varnothing =2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\times \left\{0\right\}$$
50	47 48 49	3eqtri	$$⊢\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\varnothing \right]\times \left\{1\right\}\right)\cup \left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\times \left\{0\right\}\right)=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\times \left\{0\right\}$$
51	42 50	eqtrdi	$$⊢j=0\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)=2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\times \left\{0\right\}$$
52	51	oveq2d	$$⊢j=0\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(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\times \left\{0\right\}\right)$$
53	30 52	csbie	$$⊢⦋0/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(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\times \left\{0\right\}\right)$$
54		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)$$
55	54 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)$$
56	3 55	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)$$
57		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)$$
58	56 57	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)$$
59		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\}$$
60	58 59	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\}$$
61		fvex	$$⊢2^{nd}\left(1^{st}\left(T\right)\right)\in \mathrm{V}$$
62		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)$$
63	61 62	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)$$
64	60 63	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)$$
65		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)$$
66	64 65	syl	$$⊢\phi \to 2^{nd}\left(1^{st}\left(T\right)\right):\left(1\dots N\right)\underset{onto}{⟶}\left(1\dots N\right)$$
67		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)$$
68	66 67	syl	$$⊢\phi \to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]=\left(1\dots N\right)$$
69	68	xpeq1d	$$⊢\phi \to 2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\times \left\{0\right\}=\left(1\dots N\right)\times \left\{0\right\}$$
70	69	oveq2d	$$⊢\phi \to 1^{st}\left(1^{st}\left(T\right)\right){+}_f\left(2^{nd}\left(1^{st}\left(T\right)\right)\left[\left(1\dots N\right)\right]\times \left\{0\right\}\right)=1^{st}\left(1^{st}\left(T\right)\right){+}_f\left(\left(1\dots N\right)\times \left\{0\right\}\right)$$
71	53 70	eqtrid	$$⊢\phi \to ⦋0/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\{0\right\}\right)$$
72	71	adantr	$$⊢\left(\phi \wedge y=0\right)\to ⦋0/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\{0\right\}\right)$$
73	29 72	eqtrd	$$⊢\left(\phi \wedge y=0\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\{0\right\}\right)$$
74		nnm1nn0	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{N}}_0$$
75	1 74	syl	$$⊢\phi \to N-1\in {\mathbb{N}}_0$$
76		0elfz	$$⊢N-1\in {\mathbb{N}}_0\to 0\in \left(0\dots N-1\right)$$
77	75 76	syl	$$⊢\phi \to 0\in \left(0\dots N-1\right)$$
78		ovexd	$$⊢\phi \to 1^{st}\left(1^{st}\left(T\right)\right){+}_f\left(\left(1\dots N\right)\times \left\{0\right\}\right)\in \mathrm{V}$$
79	23 73 77 78	fvmptd	$$⊢\phi \to F\left(0\right)=1^{st}\left(1^{st}\left(T\right)\right){+}_f\left(\left(1\dots N\right)\times \left\{0\right\}\right)$$
80		ovexd	$$⊢\phi \to \left(1\dots N\right)\in \mathrm{V}$$
81		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)$$
82	58 81	syl	$$⊢\phi \to 1^{st}\left(1^{st}\left(T\right)\right)\in \left({\left(0..^K\right)}^{\left(1\dots N\right)}\right)$$
83		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)$$
84	82 83	syl	$$⊢\phi \to 1^{st}\left(1^{st}\left(T\right)\right)Fn\left(1\dots N\right)$$
85		fnconstg	$$⊢0\in \mathrm{V}\to \left(\left(1\dots N\right)\times \left\{0\right\}\right)Fn\left(1\dots N\right)$$
86	30 85	mp1i	$$⊢\phi \to \left(\left(1\dots N\right)\times \left\{0\right\}\right)Fn\left(1\dots N\right)$$
87		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)$$
88	30	fvconst2	$$⊢n\in \left(1\dots N\right)\to \left(\left(1\dots N\right)\times \left\{0\right\}\right)\left(n\right)=0$$
89	88	adantl	$$⊢\left(\phi \wedge n\in \left(1\dots N\right)\right)\to \left(\left(1\dots N\right)\times \left\{0\right\}\right)\left(n\right)=0$$
90		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)$$
91	82 90	syl	$$⊢\phi \to 1^{st}\left(1^{st}\left(T\right)\right):\left(1\dots N\right)⟶\left(0..^K\right)$$
92	91	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)$$
93		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$$
94	92 93	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$$
95	94	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 ℂ$$
96	95	addridd	$$⊢\left(\phi \wedge n\in \left(1\dots N\right)\right)\to 1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)+0=1^{st}\left(1^{st}\left(T\right)\right)\left(n\right)$$
97	80 84 86 84 87 89 96	offveq	$$⊢\phi \to 1^{st}\left(1^{st}\left(T\right)\right){+}_f\left(\left(1\dots N\right)\times \left\{0\right\}\right)=1^{st}\left(1^{st}\left(T\right)\right)$$
98	79 97	eqtrd	$$⊢\phi \to F\left(0\right)=1^{st}\left(1^{st}\left(T\right)\right)$$