# Metamath Proof Explorer

## Theorem poimirlem13

Description: Lemma for poimir - for at most one simplex associated with a shared face is the opposite vertex first on the walk. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 ${⊢}{\phi }\to {N}\in ℕ$
poimirlem22.s
poimirlem22.1 ${⊢}{\phi }\to {F}:\left(0\dots {N}-1\right)⟶{\left(0\dots {K}\right)}^{\left(1\dots {N}\right)}$
Assertion poimirlem13 ${⊢}{\phi }\to {\exists }^{*}{z}\in {S}{2}^{nd}\left({z}\right)=0$

### Proof

Step Hyp Ref Expression
1 poimir.0 ${⊢}{\phi }\to {N}\in ℕ$
2 poimirlem22.s
3 poimirlem22.1 ${⊢}{\phi }\to {F}:\left(0\dots {N}-1\right)⟶{\left(0\dots {K}\right)}^{\left(1\dots {N}\right)}$
4 1 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to {N}\in ℕ$
5 3 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to {F}:\left(0\dots {N}-1\right)⟶{\left(0\dots {K}\right)}^{\left(1\dots {N}\right)}$
6 simplrl ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to {z}\in {S}$
7 simprl ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to {2}^{nd}\left({z}\right)=0$
8 4 2 5 6 7 poimirlem10 ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to {F}\left({N}-1\right){-}_{f}\left(\left(1\dots {N}\right)×\left\{1\right\}\right)={1}^{st}\left({1}^{st}\left({z}\right)\right)$
9 simplrr ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to {k}\in {S}$
10 simprr ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to {2}^{nd}\left({k}\right)=0$
11 4 2 5 9 10 poimirlem10 ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to {F}\left({N}-1\right){-}_{f}\left(\left(1\dots {N}\right)×\left\{1\right\}\right)={1}^{st}\left({1}^{st}\left({k}\right)\right)$
12 8 11 eqtr3d ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to {1}^{st}\left({1}^{st}\left({z}\right)\right)={1}^{st}\left({1}^{st}\left({k}\right)\right)$
13 elrabi
14 13 2 eleq2s ${⊢}{z}\in {S}\to {z}\in \left(\left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)×\left(0\dots {N}\right)\right)$
15 xp1st ${⊢}{z}\in \left(\left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)×\left(0\dots {N}\right)\right)\to {1}^{st}\left({z}\right)\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)$
16 14 15 syl ${⊢}{z}\in {S}\to {1}^{st}\left({z}\right)\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)$
17 xp2nd ${⊢}{1}^{st}\left({z}\right)\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\in \left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}$
18 16 17 syl ${⊢}{z}\in {S}\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\in \left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}$
19 fvex ${⊢}{2}^{nd}\left({1}^{st}\left({z}\right)\right)\in \mathrm{V}$
20 f1oeq1 ${⊢}{f}={2}^{nd}\left({1}^{st}\left({z}\right)\right)\to \left({f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)↔{2}^{nd}\left({1}^{st}\left({z}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right)$
21 19 20 elab ${⊢}{2}^{nd}\left({1}^{st}\left({z}\right)\right)\in \left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}↔{2}^{nd}\left({1}^{st}\left({z}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)$
22 18 21 sylib ${⊢}{z}\in {S}\to {2}^{nd}\left({1}^{st}\left({z}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)$
23 f1ofn ${⊢}{2}^{nd}\left({1}^{st}\left({z}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)Fn\left(1\dots {N}\right)$
24 22 23 syl ${⊢}{z}\in {S}\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)Fn\left(1\dots {N}\right)$
25 24 adantr ${⊢}\left({z}\in {S}\wedge {k}\in {S}\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)Fn\left(1\dots {N}\right)$
26 25 ad2antlr ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)Fn\left(1\dots {N}\right)$
27 elrabi
28 27 2 eleq2s ${⊢}{k}\in {S}\to {k}\in \left(\left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)×\left(0\dots {N}\right)\right)$
29 xp1st ${⊢}{k}\in \left(\left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)×\left(0\dots {N}\right)\right)\to {1}^{st}\left({k}\right)\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)$
30 28 29 syl ${⊢}{k}\in {S}\to {1}^{st}\left({k}\right)\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)$
31 xp2nd ${⊢}{1}^{st}\left({k}\right)\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)\to {2}^{nd}\left({1}^{st}\left({k}\right)\right)\in \left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}$
32 30 31 syl ${⊢}{k}\in {S}\to {2}^{nd}\left({1}^{st}\left({k}\right)\right)\in \left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}$
33 fvex ${⊢}{2}^{nd}\left({1}^{st}\left({k}\right)\right)\in \mathrm{V}$
34 f1oeq1 ${⊢}{f}={2}^{nd}\left({1}^{st}\left({k}\right)\right)\to \left({f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)↔{2}^{nd}\left({1}^{st}\left({k}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right)$
35 33 34 elab ${⊢}{2}^{nd}\left({1}^{st}\left({k}\right)\right)\in \left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}↔{2}^{nd}\left({1}^{st}\left({k}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)$
36 32 35 sylib ${⊢}{k}\in {S}\to {2}^{nd}\left({1}^{st}\left({k}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)$
37 f1ofn ${⊢}{2}^{nd}\left({1}^{st}\left({k}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\to {2}^{nd}\left({1}^{st}\left({k}\right)\right)Fn\left(1\dots {N}\right)$
38 36 37 syl ${⊢}{k}\in {S}\to {2}^{nd}\left({1}^{st}\left({k}\right)\right)Fn\left(1\dots {N}\right)$
39 38 adantl ${⊢}\left({z}\in {S}\wedge {k}\in {S}\right)\to {2}^{nd}\left({1}^{st}\left({k}\right)\right)Fn\left(1\dots {N}\right)$
40 39 ad2antlr ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to {2}^{nd}\left({1}^{st}\left({k}\right)\right)Fn\left(1\dots {N}\right)$
41 eleq1 ${⊢}{m}={n}\to \left({m}\in \left(1\dots {N}\right)↔{n}\in \left(1\dots {N}\right)\right)$
42 41 anbi2d ${⊢}{m}={n}\to \left(\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {m}\in \left(1\dots {N}\right)\right)↔\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {n}\in \left(1\dots {N}\right)\right)\right)$
43 oveq2 ${⊢}{m}={n}\to \left(1\dots {m}\right)=\left(1\dots {n}\right)$
44 43 imaeq2d ${⊢}{m}={n}\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {m}\right)\right]={2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\right]$
45 43 imaeq2d ${⊢}{m}={n}\to {2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {m}\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}\right)\right]$
46 44 45 eqeq12d ${⊢}{m}={n}\to \left({2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {m}\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {m}\right)\right]↔{2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}\right)\right]\right)$
47 42 46 imbi12d ${⊢}{m}={n}\to \left(\left(\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {m}\in \left(1\dots {N}\right)\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {m}\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {m}\right)\right]\right)↔\left(\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}\right)\right]\right)\right)$
48 1 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {m}\in \left(1\dots {N}\right)\right)\to {N}\in ℕ$
49 3 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {m}\in \left(1\dots {N}\right)\right)\to {F}:\left(0\dots {N}-1\right)⟶{\left(0\dots {K}\right)}^{\left(1\dots {N}\right)}$
50 simpl ${⊢}\left({z}\in {S}\wedge {k}\in {S}\right)\to {z}\in {S}$
51 50 ad3antlr ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {m}\in \left(1\dots {N}\right)\right)\to {z}\in {S}$
52 simplrl ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {m}\in \left(1\dots {N}\right)\right)\to {2}^{nd}\left({z}\right)=0$
53 simpr ${⊢}\left({z}\in {S}\wedge {k}\in {S}\right)\to {k}\in {S}$
54 53 ad3antlr ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {m}\in \left(1\dots {N}\right)\right)\to {k}\in {S}$
55 simplrr ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {m}\in \left(1\dots {N}\right)\right)\to {2}^{nd}\left({k}\right)=0$
56 simpr ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {m}\in \left(1\dots {N}\right)\right)\to {m}\in \left(1\dots {N}\right)$
57 48 2 49 51 52 54 55 56 poimirlem11 ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {m}\in \left(1\dots {N}\right)\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {m}\right)\right]\subseteq {2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {m}\right)\right]$
58 48 2 49 54 55 51 52 56 poimirlem11 ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {m}\in \left(1\dots {N}\right)\right)\to {2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {m}\right)\right]\subseteq {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {m}\right)\right]$
59 57 58 eqssd ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {m}\in \left(1\dots {N}\right)\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {m}\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {m}\right)\right]$
60 47 59 chvarvv ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}\right)\right]$
61 simpll ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to {\phi }$
62 elfznn ${⊢}{n}\in \left(1\dots {N}\right)\to {n}\in ℕ$
63 nnm1nn0 ${⊢}{n}\in ℕ\to {n}-1\in {ℕ}_{0}$
64 62 63 syl ${⊢}{n}\in \left(1\dots {N}\right)\to {n}-1\in {ℕ}_{0}$
65 64 adantr ${⊢}\left({n}\in \left(1\dots {N}\right)\wedge ¬{n}=1\right)\to {n}-1\in {ℕ}_{0}$
66 62 nncnd ${⊢}{n}\in \left(1\dots {N}\right)\to {n}\in ℂ$
67 ax-1cn ${⊢}1\in ℂ$
68 subeq0 ${⊢}\left({n}\in ℂ\wedge 1\in ℂ\right)\to \left({n}-1=0↔{n}=1\right)$
69 66 67 68 sylancl ${⊢}{n}\in \left(1\dots {N}\right)\to \left({n}-1=0↔{n}=1\right)$
70 69 necon3abid ${⊢}{n}\in \left(1\dots {N}\right)\to \left({n}-1\ne 0↔¬{n}=1\right)$
71 70 biimpar ${⊢}\left({n}\in \left(1\dots {N}\right)\wedge ¬{n}=1\right)\to {n}-1\ne 0$
72 elnnne0 ${⊢}{n}-1\in ℕ↔\left({n}-1\in {ℕ}_{0}\wedge {n}-1\ne 0\right)$
73 65 71 72 sylanbrc ${⊢}\left({n}\in \left(1\dots {N}\right)\wedge ¬{n}=1\right)\to {n}-1\in ℕ$
74 73 adantl ${⊢}\left({\phi }\wedge \left({n}\in \left(1\dots {N}\right)\wedge ¬{n}=1\right)\right)\to {n}-1\in ℕ$
75 64 nn0red ${⊢}{n}\in \left(1\dots {N}\right)\to {n}-1\in ℝ$
76 75 adantl ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {N}\right)\right)\to {n}-1\in ℝ$
77 62 nnred ${⊢}{n}\in \left(1\dots {N}\right)\to {n}\in ℝ$
78 77 adantl ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {N}\right)\right)\to {n}\in ℝ$
79 1 nnred ${⊢}{\phi }\to {N}\in ℝ$
80 79 adantr ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {N}\right)\right)\to {N}\in ℝ$
81 77 lem1d ${⊢}{n}\in \left(1\dots {N}\right)\to {n}-1\le {n}$
82 81 adantl ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {N}\right)\right)\to {n}-1\le {n}$
83 elfzle2 ${⊢}{n}\in \left(1\dots {N}\right)\to {n}\le {N}$
84 83 adantl ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {N}\right)\right)\to {n}\le {N}$
85 76 78 80 82 84 letrd ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {N}\right)\right)\to {n}-1\le {N}$
86 85 adantrr ${⊢}\left({\phi }\wedge \left({n}\in \left(1\dots {N}\right)\wedge ¬{n}=1\right)\right)\to {n}-1\le {N}$
87 1 nnzd ${⊢}{\phi }\to {N}\in ℤ$
88 fznn ${⊢}{N}\in ℤ\to \left({n}-1\in \left(1\dots {N}\right)↔\left({n}-1\in ℕ\wedge {n}-1\le {N}\right)\right)$
89 87 88 syl ${⊢}{\phi }\to \left({n}-1\in \left(1\dots {N}\right)↔\left({n}-1\in ℕ\wedge {n}-1\le {N}\right)\right)$
90 89 adantr ${⊢}\left({\phi }\wedge \left({n}\in \left(1\dots {N}\right)\wedge ¬{n}=1\right)\right)\to \left({n}-1\in \left(1\dots {N}\right)↔\left({n}-1\in ℕ\wedge {n}-1\le {N}\right)\right)$
91 74 86 90 mpbir2and ${⊢}\left({\phi }\wedge \left({n}\in \left(1\dots {N}\right)\wedge ¬{n}=1\right)\right)\to {n}-1\in \left(1\dots {N}\right)$
92 61 91 sylan ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge \left({n}\in \left(1\dots {N}\right)\wedge ¬{n}=1\right)\right)\to {n}-1\in \left(1\dots {N}\right)$
93 ovex ${⊢}{n}-1\in \mathrm{V}$
94 eleq1 ${⊢}{m}={n}-1\to \left({m}\in \left(1\dots {N}\right)↔{n}-1\in \left(1\dots {N}\right)\right)$
95 94 anbi2d ${⊢}{m}={n}-1\to \left(\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {m}\in \left(1\dots {N}\right)\right)↔\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {n}-1\in \left(1\dots {N}\right)\right)\right)$
96 oveq2 ${⊢}{m}={n}-1\to \left(1\dots {m}\right)=\left(1\dots {n}-1\right)$
97 96 imaeq2d ${⊢}{m}={n}-1\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {m}\right)\right]={2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]$
98 96 imaeq2d ${⊢}{m}={n}-1\to {2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {m}\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}-1\right)\right]$
99 97 98 eqeq12d ${⊢}{m}={n}-1\to \left({2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {m}\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {m}\right)\right]↔{2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}-1\right)\right]\right)$
100 95 99 imbi12d ${⊢}{m}={n}-1\to \left(\left(\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {m}\in \left(1\dots {N}\right)\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {m}\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {m}\right)\right]\right)↔\left(\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {n}-1\in \left(1\dots {N}\right)\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}-1\right)\right]\right)\right)$
101 93 100 59 vtocl ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {n}-1\in \left(1\dots {N}\right)\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}-1\right)\right]$
102 92 101 syldan ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge \left({n}\in \left(1\dots {N}\right)\wedge ¬{n}=1\right)\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}-1\right)\right]$
103 102 expr ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left(¬{n}=1\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}-1\right)\right]\right)$
104 ima0 ${⊢}{2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\varnothing \right]=\varnothing$
105 ima0 ${⊢}{2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\varnothing \right]=\varnothing$
106 104 105 eqtr4i ${⊢}{2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\varnothing \right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\varnothing \right]$
107 oveq1 ${⊢}{n}=1\to {n}-1=1-1$
108 1m1e0 ${⊢}1-1=0$
109 107 108 syl6eq ${⊢}{n}=1\to {n}-1=0$
110 109 oveq2d ${⊢}{n}=1\to \left(1\dots {n}-1\right)=\left(1\dots 0\right)$
111 fz10 ${⊢}\left(1\dots 0\right)=\varnothing$
112 110 111 syl6eq ${⊢}{n}=1\to \left(1\dots {n}-1\right)=\varnothing$
113 112 imaeq2d ${⊢}{n}=1\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]={2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\varnothing \right]$
114 112 imaeq2d ${⊢}{n}=1\to {2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}-1\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\varnothing \right]$
115 106 113 114 3eqtr4a ${⊢}{n}=1\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}-1\right)\right]$
116 103 115 pm2.61d2 ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}-1\right)\right]$
117 60 116 difeq12d ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}-1\right)\right]$
118 fnsnfv ${⊢}\left({2}^{nd}\left({1}^{st}\left({z}\right)\right)Fn\left(1\dots {N}\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left\{{2}^{nd}\left({1}^{st}\left({z}\right)\right)\left({n}\right)\right\}={2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left\{{n}\right\}\right]$
119 24 118 sylan ${⊢}\left({z}\in {S}\wedge {n}\in \left(1\dots {N}\right)\right)\to \left\{{2}^{nd}\left({1}^{st}\left({z}\right)\right)\left({n}\right)\right\}={2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left\{{n}\right\}\right]$
120 62 adantl ${⊢}\left({z}\in {S}\wedge {n}\in \left(1\dots {N}\right)\right)\to {n}\in ℕ$
121 uncom ${⊢}\left(1\dots {n}-1\right)\cup \left\{{n}\right\}=\left\{{n}\right\}\cup \left(1\dots {n}-1\right)$
122 121 difeq1i ${⊢}\left(\left(1\dots {n}-1\right)\cup \left\{{n}\right\}\right)\setminus \left(1\dots {n}-1\right)=\left(\left\{{n}\right\}\cup \left(1\dots {n}-1\right)\right)\setminus \left(1\dots {n}-1\right)$
123 difun2 ${⊢}\left(\left\{{n}\right\}\cup \left(1\dots {n}-1\right)\right)\setminus \left(1\dots {n}-1\right)=\left\{{n}\right\}\setminus \left(1\dots {n}-1\right)$
124 122 123 eqtri ${⊢}\left(\left(1\dots {n}-1\right)\cup \left\{{n}\right\}\right)\setminus \left(1\dots {n}-1\right)=\left\{{n}\right\}\setminus \left(1\dots {n}-1\right)$
125 nncn ${⊢}{n}\in ℕ\to {n}\in ℂ$
126 npcan1 ${⊢}{n}\in ℂ\to {n}-1+1={n}$
127 125 126 syl ${⊢}{n}\in ℕ\to {n}-1+1={n}$
128 elnnuz ${⊢}{n}\in ℕ↔{n}\in {ℤ}_{\ge 1}$
129 128 biimpi ${⊢}{n}\in ℕ\to {n}\in {ℤ}_{\ge 1}$
130 127 129 eqeltrd ${⊢}{n}\in ℕ\to {n}-1+1\in {ℤ}_{\ge 1}$
131 63 nn0zd ${⊢}{n}\in ℕ\to {n}-1\in ℤ$
132 uzid ${⊢}{n}-1\in ℤ\to {n}-1\in {ℤ}_{\ge \left({n}-1\right)}$
133 131 132 syl ${⊢}{n}\in ℕ\to {n}-1\in {ℤ}_{\ge \left({n}-1\right)}$
134 peano2uz ${⊢}{n}-1\in {ℤ}_{\ge \left({n}-1\right)}\to {n}-1+1\in {ℤ}_{\ge \left({n}-1\right)}$
135 133 134 syl ${⊢}{n}\in ℕ\to {n}-1+1\in {ℤ}_{\ge \left({n}-1\right)}$
136 127 135 eqeltrrd ${⊢}{n}\in ℕ\to {n}\in {ℤ}_{\ge \left({n}-1\right)}$
137 fzsplit2 ${⊢}\left({n}-1+1\in {ℤ}_{\ge 1}\wedge {n}\in {ℤ}_{\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)$
138 130 136 137 syl2anc ${⊢}{n}\in ℕ\to \left(1\dots {n}\right)=\left(1\dots {n}-1\right)\cup \left({n}-1+1\dots {n}\right)$
139 127 oveq1d ${⊢}{n}\in ℕ\to \left({n}-1+1\dots {n}\right)=\left({n}\dots {n}\right)$
140 nnz ${⊢}{n}\in ℕ\to {n}\in ℤ$
141 fzsn ${⊢}{n}\in ℤ\to \left({n}\dots {n}\right)=\left\{{n}\right\}$
142 140 141 syl ${⊢}{n}\in ℕ\to \left({n}\dots {n}\right)=\left\{{n}\right\}$
143 139 142 eqtrd ${⊢}{n}\in ℕ\to \left({n}-1+1\dots {n}\right)=\left\{{n}\right\}$
144 143 uneq2d ${⊢}{n}\in ℕ\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\}$
145 138 144 eqtrd ${⊢}{n}\in ℕ\to \left(1\dots {n}\right)=\left(1\dots {n}-1\right)\cup \left\{{n}\right\}$
146 145 difeq1d ${⊢}{n}\in ℕ\to \left(1\dots {n}\right)\setminus \left(1\dots {n}-1\right)=\left(\left(1\dots {n}-1\right)\cup \left\{{n}\right\}\right)\setminus \left(1\dots {n}-1\right)$
147 nnre ${⊢}{n}\in ℕ\to {n}\in ℝ$
148 ltm1 ${⊢}{n}\in ℝ\to {n}-1<{n}$
149 peano2rem ${⊢}{n}\in ℝ\to {n}-1\in ℝ$
150 ltnle ${⊢}\left({n}-1\in ℝ\wedge {n}\in ℝ\right)\to \left({n}-1<{n}↔¬{n}\le {n}-1\right)$
151 149 150 mpancom ${⊢}{n}\in ℝ\to \left({n}-1<{n}↔¬{n}\le {n}-1\right)$
152 148 151 mpbid ${⊢}{n}\in ℝ\to ¬{n}\le {n}-1$
153 elfzle2 ${⊢}{n}\in \left(1\dots {n}-1\right)\to {n}\le {n}-1$
154 152 153 nsyl ${⊢}{n}\in ℝ\to ¬{n}\in \left(1\dots {n}-1\right)$
155 147 154 syl ${⊢}{n}\in ℕ\to ¬{n}\in \left(1\dots {n}-1\right)$
156 incom ${⊢}\left(1\dots {n}-1\right)\cap \left\{{n}\right\}=\left\{{n}\right\}\cap \left(1\dots {n}-1\right)$
157 156 eqeq1i ${⊢}\left(1\dots {n}-1\right)\cap \left\{{n}\right\}=\varnothing ↔\left\{{n}\right\}\cap \left(1\dots {n}-1\right)=\varnothing$
158 disjsn ${⊢}\left(1\dots {n}-1\right)\cap \left\{{n}\right\}=\varnothing ↔¬{n}\in \left(1\dots {n}-1\right)$
159 disj3 ${⊢}\left\{{n}\right\}\cap \left(1\dots {n}-1\right)=\varnothing ↔\left\{{n}\right\}=\left\{{n}\right\}\setminus \left(1\dots {n}-1\right)$
160 157 158 159 3bitr3i ${⊢}¬{n}\in \left(1\dots {n}-1\right)↔\left\{{n}\right\}=\left\{{n}\right\}\setminus \left(1\dots {n}-1\right)$
161 155 160 sylib ${⊢}{n}\in ℕ\to \left\{{n}\right\}=\left\{{n}\right\}\setminus \left(1\dots {n}-1\right)$
162 124 146 161 3eqtr4a ${⊢}{n}\in ℕ\to \left(1\dots {n}\right)\setminus \left(1\dots {n}-1\right)=\left\{{n}\right\}$
163 120 162 syl ${⊢}\left({z}\in {S}\wedge {n}\in \left(1\dots {N}\right)\right)\to \left(1\dots {n}\right)\setminus \left(1\dots {n}-1\right)=\left\{{n}\right\}$
164 163 imaeq2d ${⊢}\left({z}\in {S}\wedge {n}\in \left(1\dots {N}\right)\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\setminus \left(1\dots {n}-1\right)\right]={2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left\{{n}\right\}\right]$
165 dff1o3 ${⊢}{2}^{nd}\left({1}^{st}\left({z}\right)\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)↔\left({2}^{nd}\left({1}^{st}\left({z}\right)\right):\left(1\dots {N}\right)\underset{onto}{⟶}\left(1\dots {N}\right)\wedge \mathrm{Fun}{{2}^{nd}\left({1}^{st}\left({z}\right)\right)}^{-1}\right)$
166 165 simprbi ${⊢}{2}^{nd}\left({1}^{st}\left({z}\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({z}\right)\right)}^{-1}$
167 22 166 syl ${⊢}{z}\in {S}\to \mathrm{Fun}{{2}^{nd}\left({1}^{st}\left({z}\right)\right)}^{-1}$
168 imadif ${⊢}\mathrm{Fun}{{2}^{nd}\left({1}^{st}\left({z}\right)\right)}^{-1}\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\setminus \left(1\dots {n}-1\right)\right]={2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]$
169 167 168 syl ${⊢}{z}\in {S}\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\setminus \left(1\dots {n}-1\right)\right]={2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]$
170 169 adantr ${⊢}\left({z}\in {S}\wedge {n}\in \left(1\dots {N}\right)\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\setminus \left(1\dots {n}-1\right)\right]={2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]$
171 119 164 170 3eqtr2d ${⊢}\left({z}\in {S}\wedge {n}\in \left(1\dots {N}\right)\right)\to \left\{{2}^{nd}\left({1}^{st}\left({z}\right)\right)\left({n}\right)\right\}={2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]$
172 6 171 sylan ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left\{{2}^{nd}\left({1}^{st}\left({z}\right)\right)\left({n}\right)\right\}={2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]$
173 eleq1 ${⊢}{z}={k}\to \left({z}\in {S}↔{k}\in {S}\right)$
174 173 anbi1d ${⊢}{z}={k}\to \left(\left({z}\in {S}\wedge {n}\in \left(1\dots {N}\right)\right)↔\left({k}\in {S}\wedge {n}\in \left(1\dots {N}\right)\right)\right)$
175 2fveq3 ${⊢}{z}={k}\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)={2}^{nd}\left({1}^{st}\left({k}\right)\right)$
176 175 fveq1d ${⊢}{z}={k}\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left({n}\right)={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left({n}\right)$
177 176 sneqd ${⊢}{z}={k}\to \left\{{2}^{nd}\left({1}^{st}\left({z}\right)\right)\left({n}\right)\right\}=\left\{{2}^{nd}\left({1}^{st}\left({k}\right)\right)\left({n}\right)\right\}$
178 175 imaeq1d ${⊢}{z}={k}\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}\right)\right]$
179 175 imaeq1d ${⊢}{z}={k}\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}-1\right)\right]$
180 178 179 difeq12d ${⊢}{z}={k}\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}-1\right)\right]$
181 177 180 eqeq12d ${⊢}{z}={k}\to \left(\left\{{2}^{nd}\left({1}^{st}\left({z}\right)\right)\left({n}\right)\right\}={2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]↔\left\{{2}^{nd}\left({1}^{st}\left({k}\right)\right)\left({n}\right)\right\}={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}-1\right)\right]\right)$
182 174 181 imbi12d ${⊢}{z}={k}\to \left(\left(\left({z}\in {S}\wedge {n}\in \left(1\dots {N}\right)\right)\to \left\{{2}^{nd}\left({1}^{st}\left({z}\right)\right)\left({n}\right)\right\}={2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left[\left(1\dots {n}-1\right)\right]\right)↔\left(\left({k}\in {S}\wedge {n}\in \left(1\dots {N}\right)\right)\to \left\{{2}^{nd}\left({1}^{st}\left({k}\right)\right)\left({n}\right)\right\}={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}-1\right)\right]\right)\right)$
183 182 171 chvarvv ${⊢}\left({k}\in {S}\wedge {n}\in \left(1\dots {N}\right)\right)\to \left\{{2}^{nd}\left({1}^{st}\left({k}\right)\right)\left({n}\right)\right\}={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}-1\right)\right]$
184 9 183 sylan ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left\{{2}^{nd}\left({1}^{st}\left({k}\right)\right)\left({n}\right)\right\}={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}\right)\right]\setminus {2}^{nd}\left({1}^{st}\left({k}\right)\right)\left[\left(1\dots {n}-1\right)\right]$
185 117 172 184 3eqtr4d ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to \left\{{2}^{nd}\left({1}^{st}\left({z}\right)\right)\left({n}\right)\right\}=\left\{{2}^{nd}\left({1}^{st}\left({k}\right)\right)\left({n}\right)\right\}$
186 fvex ${⊢}{2}^{nd}\left({1}^{st}\left({z}\right)\right)\left({n}\right)\in \mathrm{V}$
187 186 sneqr ${⊢}\left\{{2}^{nd}\left({1}^{st}\left({z}\right)\right)\left({n}\right)\right\}=\left\{{2}^{nd}\left({1}^{st}\left({k}\right)\right)\left({n}\right)\right\}\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left({n}\right)={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left({n}\right)$
188 185 187 syl ${⊢}\left(\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\wedge {n}\in \left(1\dots {N}\right)\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)\left({n}\right)={2}^{nd}\left({1}^{st}\left({k}\right)\right)\left({n}\right)$
189 26 40 188 eqfnfvd ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to {2}^{nd}\left({1}^{st}\left({z}\right)\right)={2}^{nd}\left({1}^{st}\left({k}\right)\right)$
190 xpopth ${⊢}\left({1}^{st}\left({z}\right)\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)\wedge {1}^{st}\left({k}\right)\in \left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)\right)\to \left(\left({1}^{st}\left({1}^{st}\left({z}\right)\right)={1}^{st}\left({1}^{st}\left({k}\right)\right)\wedge {2}^{nd}\left({1}^{st}\left({z}\right)\right)={2}^{nd}\left({1}^{st}\left({k}\right)\right)\right)↔{1}^{st}\left({z}\right)={1}^{st}\left({k}\right)\right)$
191 16 30 190 syl2an ${⊢}\left({z}\in {S}\wedge {k}\in {S}\right)\to \left(\left({1}^{st}\left({1}^{st}\left({z}\right)\right)={1}^{st}\left({1}^{st}\left({k}\right)\right)\wedge {2}^{nd}\left({1}^{st}\left({z}\right)\right)={2}^{nd}\left({1}^{st}\left({k}\right)\right)\right)↔{1}^{st}\left({z}\right)={1}^{st}\left({k}\right)\right)$
192 191 ad2antlr ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to \left(\left({1}^{st}\left({1}^{st}\left({z}\right)\right)={1}^{st}\left({1}^{st}\left({k}\right)\right)\wedge {2}^{nd}\left({1}^{st}\left({z}\right)\right)={2}^{nd}\left({1}^{st}\left({k}\right)\right)\right)↔{1}^{st}\left({z}\right)={1}^{st}\left({k}\right)\right)$
193 12 189 192 mpbi2and ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to {1}^{st}\left({z}\right)={1}^{st}\left({k}\right)$
194 eqtr3 ${⊢}\left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\to {2}^{nd}\left({z}\right)={2}^{nd}\left({k}\right)$
195 194 adantl ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to {2}^{nd}\left({z}\right)={2}^{nd}\left({k}\right)$
196 xpopth ${⊢}\left({z}\in \left(\left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)×\left(0\dots {N}\right)\right)\wedge {k}\in \left(\left(\left({\left(0..^{K}\right)}^{\left(1\dots {N}\right)}\right)×\left\{{f}|{f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\right\}\right)×\left(0\dots {N}\right)\right)\right)\to \left(\left({1}^{st}\left({z}\right)={1}^{st}\left({k}\right)\wedge {2}^{nd}\left({z}\right)={2}^{nd}\left({k}\right)\right)↔{z}={k}\right)$
197 14 28 196 syl2an ${⊢}\left({z}\in {S}\wedge {k}\in {S}\right)\to \left(\left({1}^{st}\left({z}\right)={1}^{st}\left({k}\right)\wedge {2}^{nd}\left({z}\right)={2}^{nd}\left({k}\right)\right)↔{z}={k}\right)$
198 197 ad2antlr ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to \left(\left({1}^{st}\left({z}\right)={1}^{st}\left({k}\right)\wedge {2}^{nd}\left({z}\right)={2}^{nd}\left({k}\right)\right)↔{z}={k}\right)$
199 193 195 198 mpbi2and ${⊢}\left(\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\wedge \left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\right)\to {z}={k}$
200 199 ex ${⊢}\left({\phi }\wedge \left({z}\in {S}\wedge {k}\in {S}\right)\right)\to \left(\left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\to {z}={k}\right)$
201 200 ralrimivva ${⊢}{\phi }\to \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\forall {k}\in {S}\phantom{\rule{.4em}{0ex}}\left(\left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\to {z}={k}\right)$
202 fveqeq2 ${⊢}{z}={k}\to \left({2}^{nd}\left({z}\right)=0↔{2}^{nd}\left({k}\right)=0\right)$
203 202 rmo4 ${⊢}{\exists }^{*}{z}\in {S}{2}^{nd}\left({z}\right)=0↔\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\forall {k}\in {S}\phantom{\rule{.4em}{0ex}}\left(\left({2}^{nd}\left({z}\right)=0\wedge {2}^{nd}\left({k}\right)=0\right)\to {z}={k}\right)$
204 201 203 sylibr ${⊢}{\phi }\to {\exists }^{*}{z}\in {S}{2}^{nd}\left({z}\right)=0$