poimirlem14

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

	Ref	Expression
Hypotheses	poimir.0	$⊢ φ \to N \in ℕ$
	poimirlem22.s	$⊢ S = \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\}$
	poimirlem22.1	$⊢ φ \to F : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
Assertion	poimirlem14	$⊢ φ \to \exists^{*} z \in S 2^{nd} (z) = N$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$⊢ φ \to N \in ℕ$
2		poimirlem22.s	$⊢ S = \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\}$
3		poimirlem22.1	$⊢ φ \to F : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
4	1	ad2antrr	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to N \in ℕ$
5		simplrl	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to z \in S$
6	1	nngt0d	$⊢ φ \to 0 < N$
7		breq2	$⊢ 2^{nd} (z) = N \to (0 < 2^{nd} (z) \leftrightarrow 0 < N)$
8	7	biimparc	$⊢ (0 < N \land 2^{nd} (z) = N) \to 0 < 2^{nd} (z)$
9	6 8	sylan	$⊢ (φ \land 2^{nd} (z) = N) \to 0 < 2^{nd} (z)$
10	9	ad2ant2r	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to 0 < 2^{nd} (z)$
11	4 2 5 10	poimirlem5	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to F (0) = 1^{st} (1^{st} (z))$
12		simplrr	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to k \in S$
13		breq2	$⊢ 2^{nd} (k) = N \to (0 < 2^{nd} (k) \leftrightarrow 0 < N)$
14	13	biimparc	$⊢ (0 < N \land 2^{nd} (k) = N) \to 0 < 2^{nd} (k)$
15	6 14	sylan	$⊢ (φ \land 2^{nd} (k) = N) \to 0 < 2^{nd} (k)$
16	15	ad2ant2rl	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to 0 < 2^{nd} (k)$
17	4 2 12 16	poimirlem5	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to F (0) = 1^{st} (1^{st} (k))$
18	11 17	eqtr3d	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to 1^{st} (1^{st} (z)) = 1^{st} (1^{st} (k))$
19		elrabi	$⊢ z \in \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\} \to z \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
20	19 2	eleq2s	$⊢ z \in S \to z \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
21		xp1st	$⊢ z \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \to 1^{st} (z) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
22		xp2nd	$⊢ 1^{st} (z) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 2^{nd} (1^{st} (z)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
23	20 21 22	3syl	$⊢ z \in S \to 2^{nd} (1^{st} (z)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
24		fvex	$⊢ 2^{nd} (1^{st} (z)) \in V$
25		f1oeq1	$⊢ f = 2^{nd} (1^{st} (z)) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
26	24 25	elab	$⊢ 2^{nd} (1^{st} (z)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
27	23 26	sylib	$⊢ z \in S \to 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
28		f1ofn	$⊢ 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (z)) Fn (1 \dots N)$
29	27 28	syl	$⊢ z \in S \to 2^{nd} (1^{st} (z)) Fn (1 \dots N)$
30	29	adantr	$⊢ (z \in S \land k \in S) \to 2^{nd} (1^{st} (z)) Fn (1 \dots N)$
31	30	ad2antlr	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to 2^{nd} (1^{st} (z)) Fn (1 \dots N)$
32		elrabi	$⊢ k \in \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\} \to k \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
33	32 2	eleq2s	$⊢ k \in S \to k \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
34		xp1st	$⊢ k \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \to 1^{st} (k) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
35		xp2nd	$⊢ 1^{st} (k) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 2^{nd} (1^{st} (k)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
36	33 34 35	3syl	$⊢ k \in S \to 2^{nd} (1^{st} (k)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
37		fvex	$⊢ 2^{nd} (1^{st} (k)) \in V$
38		f1oeq1	$⊢ f = 2^{nd} (1^{st} (k)) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow 2^{nd} (1^{st} (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
39	37 38	elab	$⊢ 2^{nd} (1^{st} (k)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow 2^{nd} (1^{st} (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
40	36 39	sylib	$⊢ k \in S \to 2^{nd} (1^{st} (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
41		f1ofn	$⊢ 2^{nd} (1^{st} (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (k)) Fn (1 \dots N)$
42	40 41	syl	$⊢ k \in S \to 2^{nd} (1^{st} (k)) Fn (1 \dots N)$
43	42	adantl	$⊢ (z \in S \land k \in S) \to 2^{nd} (1^{st} (k)) Fn (1 \dots N)$
44	43	ad2antlr	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to 2^{nd} (1^{st} (k)) Fn (1 \dots N)$
45		simpllr	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n \in (1 \dots N)) \to (z \in S \land k \in S)$
46		oveq2	$⊢ n = N \to (1 \dots n) = (1 \dots N)$
47	46	imaeq2d	$⊢ n = N \to 2^{nd} (1^{st} (z)) [(1 \dots n)] = 2^{nd} (1^{st} (z)) [(1 \dots N)]$
48		f1ofo	$⊢ 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
49		foima	$⊢ 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (z)) [(1 \dots N)] = (1 \dots N)$
50	27 48 49	3syl	$⊢ z \in S \to 2^{nd} (1^{st} (z)) [(1 \dots N)] = (1 \dots N)$
51	47 50	sylan9eqr	$⊢ (z \in S \land n = N) \to 2^{nd} (1^{st} (z)) [(1 \dots n)] = (1 \dots N)$
52	51	adantlr	$⊢ ((z \in S \land k \in S) \land n = N) \to 2^{nd} (1^{st} (z)) [(1 \dots n)] = (1 \dots N)$
53	46	imaeq2d	$⊢ n = N \to 2^{nd} (1^{st} (k)) [(1 \dots n)] = 2^{nd} (1^{st} (k)) [(1 \dots N)]$
54		f1ofo	$⊢ 2^{nd} (1^{st} (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (k)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
55		foima	$⊢ 2^{nd} (1^{st} (k)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (k)) [(1 \dots N)] = (1 \dots N)$
56	40 54 55	3syl	$⊢ k \in S \to 2^{nd} (1^{st} (k)) [(1 \dots N)] = (1 \dots N)$
57	53 56	sylan9eqr	$⊢ (k \in S \land n = N) \to 2^{nd} (1^{st} (k)) [(1 \dots n)] = (1 \dots N)$
58	57	adantll	$⊢ ((z \in S \land k \in S) \land n = N) \to 2^{nd} (1^{st} (k)) [(1 \dots n)] = (1 \dots N)$
59	52 58	eqtr4d	$⊢ ((z \in S \land k \in S) \land n = N) \to 2^{nd} (1^{st} (z)) [(1 \dots n)] = 2^{nd} (1^{st} (k)) [(1 \dots n)]$
60	45 59	sylan	$⊢ ((((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n \in (1 \dots N)) \land n = N) \to 2^{nd} (1^{st} (z)) [(1 \dots n)] = 2^{nd} (1^{st} (k)) [(1 \dots n)]$
61		simpll	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to φ$
62		elnnuz	$⊢ N \in ℕ \leftrightarrow N \in ℤ_{\geq 1}$
63	1 62	sylib	$⊢ φ \to N \in ℤ_{\geq 1}$
64		fzm1	$⊢ N \in ℤ_{\geq 1} \to (n \in (1 \dots N) \leftrightarrow (n \in (1 \dots N - 1) \lor n = N))$
65	63 64	syl	$⊢ φ \to (n \in (1 \dots N) \leftrightarrow (n \in (1 \dots N - 1) \lor n = N))$
66	65	anbi1d	$⊢ φ \to ((n \in (1 \dots N) \land n \neq N) \leftrightarrow ((n \in (1 \dots N - 1) \lor n = N) \land n \neq N))$
67	66	biimpa	$⊢ (φ \land (n \in (1 \dots N) \land n \neq N)) \to ((n \in (1 \dots N - 1) \lor n = N) \land n \neq N)$
68		df-ne	$⊢ n \neq N \leftrightarrow \neg n = N$
69	68	anbi2i	$⊢ ((n \in (1 \dots N - 1) \lor n = N) \land n \neq N) \leftrightarrow ((n \in (1 \dots N - 1) \lor n = N) \land \neg n = N)$
70		pm5.61	$⊢ ((n \in (1 \dots N - 1) \lor n = N) \land \neg n = N) \leftrightarrow (n \in (1 \dots N - 1) \land \neg n = N)$
71	69 70	bitri	$⊢ ((n \in (1 \dots N - 1) \lor n = N) \land n \neq N) \leftrightarrow (n \in (1 \dots N - 1) \land \neg n = N)$
72	67 71	sylib	$⊢ (φ \land (n \in (1 \dots N) \land n \neq N)) \to (n \in (1 \dots N - 1) \land \neg n = N)$
73		fz1ssfz0	$⊢ (1 \dots N - 1) \subseteq (0 \dots N - 1)$
74	73	sseli	$⊢ n \in (1 \dots N - 1) \to n \in (0 \dots N - 1)$
75	74	adantr	$⊢ (n \in (1 \dots N - 1) \land \neg n = N) \to n \in (0 \dots N - 1)$
76	72 75	syl	$⊢ (φ \land (n \in (1 \dots N) \land n \neq N)) \to n \in (0 \dots N - 1)$
77	61 76	sylan	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land (n \in (1 \dots N) \land n \neq N)) \to n \in (0 \dots N - 1)$
78		eleq1	$⊢ m = n \to (m \in (0 \dots N - 1) \leftrightarrow n \in (0 \dots N - 1))$
79	78	anbi2d	$⊢ m = n \to ((((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land m \in (0 \dots N - 1)) \leftrightarrow (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n \in (0 \dots N - 1)))$
80		oveq2	$⊢ m = n \to (1 \dots m) = (1 \dots n)$
81	80	imaeq2d	$⊢ m = n \to 2^{nd} (1^{st} (z)) [(1 \dots m)] = 2^{nd} (1^{st} (z)) [(1 \dots n)]$
82	80	imaeq2d	$⊢ m = n \to 2^{nd} (1^{st} (k)) [(1 \dots m)] = 2^{nd} (1^{st} (k)) [(1 \dots n)]$
83	81 82	eqeq12d	$⊢ m = n \to (2^{nd} (1^{st} (z)) [(1 \dots m)] = 2^{nd} (1^{st} (k)) [(1 \dots m)] \leftrightarrow 2^{nd} (1^{st} (z)) [(1 \dots n)] = 2^{nd} (1^{st} (k)) [(1 \dots n)])$
84	79 83	imbi12d	$⊢ m = n \to (((((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land m \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (z)) [(1 \dots m)] = 2^{nd} (1^{st} (k)) [(1 \dots m)]) \leftrightarrow ((((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (z)) [(1 \dots n)] = 2^{nd} (1^{st} (k)) [(1 \dots n)]))$
85	1	ad3antrrr	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land m \in (0 \dots N - 1)) \to N \in ℕ$
86	3	ad3antrrr	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land m \in (0 \dots N - 1)) \to F : (0 \dots N - 1) ⟶ {(0 \dots K)}^{(1 \dots N)}$
87		simpl	$⊢ (z \in S \land k \in S) \to z \in S$
88	87	ad3antlr	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land m \in (0 \dots N - 1)) \to z \in S$
89		simplrl	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land m \in (0 \dots N - 1)) \to 2^{nd} (z) = N$
90		simpr	$⊢ (z \in S \land k \in S) \to k \in S$
91	90	ad3antlr	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land m \in (0 \dots N - 1)) \to k \in S$
92		simplrr	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land m \in (0 \dots N - 1)) \to 2^{nd} (k) = N$
93		simpr	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land m \in (0 \dots N - 1)) \to m \in (0 \dots N - 1)$
94	85 2 86 88 89 91 92 93	poimirlem12	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land m \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (z)) [(1 \dots m)] \subseteq 2^{nd} (1^{st} (k)) [(1 \dots m)]$
95	85 2 86 91 92 88 89 93	poimirlem12	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land m \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (k)) [(1 \dots m)] \subseteq 2^{nd} (1^{st} (z)) [(1 \dots m)]$
96	94 95	eqssd	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land m \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (z)) [(1 \dots m)] = 2^{nd} (1^{st} (k)) [(1 \dots m)]$
97	84 96	chvarvv	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (z)) [(1 \dots n)] = 2^{nd} (1^{st} (k)) [(1 \dots n)]$
98	77 97	syldan	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land (n \in (1 \dots N) \land n \neq N)) \to 2^{nd} (1^{st} (z)) [(1 \dots n)] = 2^{nd} (1^{st} (k)) [(1 \dots n)]$
99	98	anassrs	$⊢ ((((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n \in (1 \dots N)) \land n \neq N) \to 2^{nd} (1^{st} (z)) [(1 \dots n)] = 2^{nd} (1^{st} (k)) [(1 \dots n)]$
100	60 99	pm2.61dane	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n \in (1 \dots N)) \to 2^{nd} (1^{st} (z)) [(1 \dots n)] = 2^{nd} (1^{st} (k)) [(1 \dots n)]$
101		simpr	$⊢ (φ \land n \in (1 \dots N)) \to n \in (1 \dots N)$
102		elfzelz	$⊢ n \in (1 \dots N) \to n \in ℤ$
103	1	nnzd	$⊢ φ \to N \in ℤ$
104		elfzm1b	$⊢ (n \in ℤ \land N \in ℤ) \to (n \in (1 \dots N) \leftrightarrow n - 1 \in (0 \dots N - 1))$
105	102 103 104	syl2anr	$⊢ (φ \land n \in (1 \dots N)) \to (n \in (1 \dots N) \leftrightarrow n - 1 \in (0 \dots N - 1))$
106	101 105	mpbid	$⊢ (φ \land n \in (1 \dots N)) \to n - 1 \in (0 \dots N - 1)$
107	61 106	sylan	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n \in (1 \dots N)) \to n - 1 \in (0 \dots N - 1)$
108		ovex	$⊢ n - 1 \in V$
109		eleq1	$⊢ m = n - 1 \to (m \in (0 \dots N - 1) \leftrightarrow n - 1 \in (0 \dots N - 1))$
110	109	anbi2d	$⊢ m = n - 1 \to ((((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land m \in (0 \dots N - 1)) \leftrightarrow (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n - 1 \in (0 \dots N - 1)))$
111		oveq2	$⊢ m = n - 1 \to (1 \dots m) = (1 \dots n - 1)$
112	111	imaeq2d	$⊢ m = n - 1 \to 2^{nd} (1^{st} (z)) [(1 \dots m)] = 2^{nd} (1^{st} (z)) [(1 \dots n - 1)]$
113	111	imaeq2d	$⊢ m = n - 1 \to 2^{nd} (1^{st} (k)) [(1 \dots m)] = 2^{nd} (1^{st} (k)) [(1 \dots n - 1)]$
114	112 113	eqeq12d	$⊢ m = n - 1 \to (2^{nd} (1^{st} (z)) [(1 \dots m)] = 2^{nd} (1^{st} (k)) [(1 \dots m)] \leftrightarrow 2^{nd} (1^{st} (z)) [(1 \dots n - 1)] = 2^{nd} (1^{st} (k)) [(1 \dots n - 1)])$
115	110 114	imbi12d	$⊢ m = n - 1 \to (((((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land m \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (z)) [(1 \dots m)] = 2^{nd} (1^{st} (k)) [(1 \dots m)]) \leftrightarrow ((((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n - 1 \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (z)) [(1 \dots n - 1)] = 2^{nd} (1^{st} (k)) [(1 \dots n - 1)]))$
116	108 115 96	vtocl	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n - 1 \in (0 \dots N - 1)) \to 2^{nd} (1^{st} (z)) [(1 \dots n - 1)] = 2^{nd} (1^{st} (k)) [(1 \dots n - 1)]$
117	107 116	syldan	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n \in (1 \dots N)) \to 2^{nd} (1^{st} (z)) [(1 \dots n - 1)] = 2^{nd} (1^{st} (k)) [(1 \dots n - 1)]$
118	100 117	difeq12d	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n \in (1 \dots N)) \to 2^{nd} (1^{st} (z)) [(1 \dots n)] ∖ 2^{nd} (1^{st} (z)) [(1 \dots n - 1)] = 2^{nd} (1^{st} (k)) [(1 \dots n)] ∖ 2^{nd} (1^{st} (k)) [(1 \dots n - 1)]$
119		fnsnfv	$⊢ (2^{nd} (1^{st} (z)) Fn (1 \dots N) \land n \in (1 \dots N)) \to \{2^{nd} (1^{st} (z)) (n)\} = 2^{nd} (1^{st} (z)) [\{n\}]$
120	29 119	sylan	$⊢ (z \in S \land n \in (1 \dots N)) \to \{2^{nd} (1^{st} (z)) (n)\} = 2^{nd} (1^{st} (z)) [\{n\}]$
121		elfznn	$⊢ n \in (1 \dots N) \to n \in ℕ$
122		uncom	$⊢ (1 \dots n - 1) \cup \{n\} = \{n\} \cup (1 \dots n - 1)$
123	122	difeq1i	$⊢ ((1 \dots n - 1) \cup \{n\}) ∖ (1 \dots n - 1) = (\{n\} \cup (1 \dots n - 1)) ∖ (1 \dots n - 1)$
124		difun2	$⊢ (\{n\} \cup (1 \dots n - 1)) ∖ (1 \dots n - 1) = \{n\} ∖ (1 \dots n - 1)$
125	123 124	eqtri	$⊢ ((1 \dots n - 1) \cup \{n\}) ∖ (1 \dots n - 1) = \{n\} ∖ (1 \dots n - 1)$
126		nncn	$⊢ n \in ℕ \to n \in ℂ$
127		npcan1	$⊢ n \in ℂ \to n - 1 + 1 = n$
128	126 127	syl	$⊢ n \in ℕ \to n - 1 + 1 = n$
129		elnnuz	$⊢ n \in ℕ \leftrightarrow n \in ℤ_{\geq 1}$
130	129	biimpi	$⊢ n \in ℕ \to n \in ℤ_{\geq 1}$
131	128 130	eqeltrd	$⊢ n \in ℕ \to n - 1 + 1 \in ℤ_{\geq 1}$
132		nnm1nn0	$⊢ n \in ℕ \to n - 1 \in ℕ_{0}$
133	132	nn0zd	$⊢ n \in ℕ \to n - 1 \in ℤ$
134		uzid	$⊢ n - 1 \in ℤ \to n - 1 \in ℤ_{\geq (n - 1)}$
135		peano2uz	$⊢ n - 1 \in ℤ_{\geq (n - 1)} \to n - 1 + 1 \in ℤ_{\geq (n - 1)}$
136	133 134 135	3syl	$⊢ n \in ℕ \to n - 1 + 1 \in ℤ_{\geq (n - 1)}$
137	128 136	eqeltrrd	$⊢ n \in ℕ \to n \in ℤ_{\geq (n - 1)}$
138		fzsplit2	$⊢ (n - 1 + 1 \in ℤ_{\geq 1} \land n \in ℤ_{\geq (n - 1)}) \to (1 \dots n) = (1 \dots n - 1) \cup (n - 1 + 1 \dots n)$
139	131 137 138	syl2anc	$⊢ n \in ℕ \to (1 \dots n) = (1 \dots n - 1) \cup (n - 1 + 1 \dots n)$
140	128	oveq1d	$⊢ n \in ℕ \to (n - 1 + 1 \dots n) = (n \dots n)$
141		nnz	$⊢ n \in ℕ \to n \in ℤ$
142		fzsn	$⊢ n \in ℤ \to (n \dots n) = \{n\}$
143	141 142	syl	$⊢ n \in ℕ \to (n \dots n) = \{n\}$
144	140 143	eqtrd	$⊢ n \in ℕ \to (n - 1 + 1 \dots n) = \{n\}$
145	144	uneq2d	$⊢ n \in ℕ \to (1 \dots n - 1) \cup (n - 1 + 1 \dots n) = (1 \dots n - 1) \cup \{n\}$
146	139 145	eqtrd	$⊢ n \in ℕ \to (1 \dots n) = (1 \dots n - 1) \cup \{n\}$
147	146	difeq1d	$⊢ n \in ℕ \to (1 \dots n) ∖ (1 \dots n - 1) = ((1 \dots n - 1) \cup \{n\}) ∖ (1 \dots n - 1)$
148		nnre	$⊢ n \in ℕ \to n \in ℝ$
149		ltm1	$⊢ n \in ℝ \to n - 1 < n$
150		peano2rem	$⊢ n \in ℝ \to n - 1 \in ℝ$
151		ltnle	$⊢ (n - 1 \in ℝ \land n \in ℝ) \to (n - 1 < n \leftrightarrow \neg n \leq n - 1)$
152	150 151	mpancom	$⊢ n \in ℝ \to (n - 1 < n \leftrightarrow \neg n \leq n - 1)$
153	149 152	mpbid	$⊢ n \in ℝ \to \neg n \leq n - 1$
154		elfzle2	$⊢ n \in (1 \dots n - 1) \to n \leq n - 1$
155	153 154	nsyl	$⊢ n \in ℝ \to \neg n \in (1 \dots n - 1)$
156	148 155	syl	$⊢ n \in ℕ \to \neg n \in (1 \dots n - 1)$
157		incom	$⊢ (1 \dots n - 1) \cap \{n\} = \{n\} \cap (1 \dots n - 1)$
158	157	eqeq1i	$⊢ (1 \dots n - 1) \cap \{n\} = \emptyset \leftrightarrow \{n\} \cap (1 \dots n - 1) = \emptyset$
159		disjsn	$⊢ (1 \dots n - 1) \cap \{n\} = \emptyset \leftrightarrow \neg n \in (1 \dots n - 1)$
160		disj3	$⊢ \{n\} \cap (1 \dots n - 1) = \emptyset \leftrightarrow \{n\} = \{n\} ∖ (1 \dots n - 1)$
161	158 159 160	3bitr3i	$⊢ \neg n \in (1 \dots n - 1) \leftrightarrow \{n\} = \{n\} ∖ (1 \dots n - 1)$
162	156 161	sylib	$⊢ n \in ℕ \to \{n\} = \{n\} ∖ (1 \dots n - 1)$
163	125 147 162	3eqtr4a	$⊢ n \in ℕ \to (1 \dots n) ∖ (1 \dots n - 1) = \{n\}$
164	121 163	syl	$⊢ n \in (1 \dots N) \to (1 \dots n) ∖ (1 \dots n - 1) = \{n\}$
165	164	imaeq2d	$⊢ n \in (1 \dots N) \to 2^{nd} (1^{st} (z)) [(1 \dots n) ∖ (1 \dots n - 1)] = 2^{nd} (1^{st} (z)) [\{n\}]$
166	165	adantl	$⊢ (z \in S \land n \in (1 \dots N)) \to 2^{nd} (1^{st} (z)) [(1 \dots n) ∖ (1 \dots n - 1)] = 2^{nd} (1^{st} (z)) [\{n\}]$
167		dff1o3	$⊢ 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow (2^{nd} (1^{st} (z)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \land Fun {2^{nd} (1^{st} (z))}^{-1})$
168	167	simprbi	$⊢ 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun {2^{nd} (1^{st} (z))}^{-1}$
169		imadif	$⊢ Fun {2^{nd} (1^{st} (z))}^{-1} \to 2^{nd} (1^{st} (z)) [(1 \dots n) ∖ (1 \dots n - 1)] = 2^{nd} (1^{st} (z)) [(1 \dots n)] ∖ 2^{nd} (1^{st} (z)) [(1 \dots n - 1)]$
170	27 168 169	3syl	$⊢ z \in S \to 2^{nd} (1^{st} (z)) [(1 \dots n) ∖ (1 \dots n - 1)] = 2^{nd} (1^{st} (z)) [(1 \dots n)] ∖ 2^{nd} (1^{st} (z)) [(1 \dots n - 1)]$
171	170	adantr	$⊢ (z \in S \land n \in (1 \dots N)) \to 2^{nd} (1^{st} (z)) [(1 \dots n) ∖ (1 \dots n - 1)] = 2^{nd} (1^{st} (z)) [(1 \dots n)] ∖ 2^{nd} (1^{st} (z)) [(1 \dots n - 1)]$
172	120 166 171	3eqtr2d	$⊢ (z \in S \land n \in (1 \dots N)) \to \{2^{nd} (1^{st} (z)) (n)\} = 2^{nd} (1^{st} (z)) [(1 \dots n)] ∖ 2^{nd} (1^{st} (z)) [(1 \dots n - 1)]$
173	5 172	sylan	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n \in (1 \dots N)) \to \{2^{nd} (1^{st} (z)) (n)\} = 2^{nd} (1^{st} (z)) [(1 \dots n)] ∖ 2^{nd} (1^{st} (z)) [(1 \dots n - 1)]$
174		eleq1	$⊢ z = k \to (z \in S \leftrightarrow k \in S)$
175	174	anbi1d	$⊢ z = k \to ((z \in S \land n \in (1 \dots N)) \leftrightarrow (k \in S \land n \in (1 \dots N)))$
176		2fveq3	$⊢ z = k \to 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (k))$
177	176	fveq1d	$⊢ z = k \to 2^{nd} (1^{st} (z)) (n) = 2^{nd} (1^{st} (k)) (n)$
178	177	sneqd	$⊢ z = k \to \{2^{nd} (1^{st} (z)) (n)\} = \{2^{nd} (1^{st} (k)) (n)\}$
179	176	imaeq1d	$⊢ z = k \to 2^{nd} (1^{st} (z)) [(1 \dots n)] = 2^{nd} (1^{st} (k)) [(1 \dots n)]$
180	176	imaeq1d	$⊢ z = k \to 2^{nd} (1^{st} (z)) [(1 \dots n - 1)] = 2^{nd} (1^{st} (k)) [(1 \dots n - 1)]$
181	179 180	difeq12d	$⊢ z = k \to 2^{nd} (1^{st} (z)) [(1 \dots n)] ∖ 2^{nd} (1^{st} (z)) [(1 \dots n - 1)] = 2^{nd} (1^{st} (k)) [(1 \dots n)] ∖ 2^{nd} (1^{st} (k)) [(1 \dots n - 1)]$
182	178 181	eqeq12d	$⊢ z = k \to (\{2^{nd} (1^{st} (z)) (n)\} = 2^{nd} (1^{st} (z)) [(1 \dots n)] ∖ 2^{nd} (1^{st} (z)) [(1 \dots n - 1)] \leftrightarrow \{2^{nd} (1^{st} (k)) (n)\} = 2^{nd} (1^{st} (k)) [(1 \dots n)] ∖ 2^{nd} (1^{st} (k)) [(1 \dots n - 1)])$
183	175 182	imbi12d	$⊢ z = k \to (((z \in S \land n \in (1 \dots N)) \to \{2^{nd} (1^{st} (z)) (n)\} = 2^{nd} (1^{st} (z)) [(1 \dots n)] ∖ 2^{nd} (1^{st} (z)) [(1 \dots n - 1)]) \leftrightarrow ((k \in S \land n \in (1 \dots N)) \to \{2^{nd} (1^{st} (k)) (n)\} = 2^{nd} (1^{st} (k)) [(1 \dots n)] ∖ 2^{nd} (1^{st} (k)) [(1 \dots n - 1)]))$
184	183 172	chvarvv	$⊢ (k \in S \land n \in (1 \dots N)) \to \{2^{nd} (1^{st} (k)) (n)\} = 2^{nd} (1^{st} (k)) [(1 \dots n)] ∖ 2^{nd} (1^{st} (k)) [(1 \dots n - 1)]$
185	12 184	sylan	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n \in (1 \dots N)) \to \{2^{nd} (1^{st} (k)) (n)\} = 2^{nd} (1^{st} (k)) [(1 \dots n)] ∖ 2^{nd} (1^{st} (k)) [(1 \dots n - 1)]$
186	118 173 185	3eqtr4d	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n \in (1 \dots N)) \to \{2^{nd} (1^{st} (z)) (n)\} = \{2^{nd} (1^{st} (k)) (n)\}$
187		fvex	$⊢ 2^{nd} (1^{st} (z)) (n) \in V$
188	187	sneqr	$⊢ \{2^{nd} (1^{st} (z)) (n)\} = \{2^{nd} (1^{st} (k)) (n)\} \to 2^{nd} (1^{st} (z)) (n) = 2^{nd} (1^{st} (k)) (n)$
189	186 188	syl	$⊢ (((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \land n \in (1 \dots N)) \to 2^{nd} (1^{st} (z)) (n) = 2^{nd} (1^{st} (k)) (n)$
190	31 44 189	eqfnfvd	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (k))$
191	20 21	syl	$⊢ z \in S \to 1^{st} (z) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
192	33 34	syl	$⊢ k \in S \to 1^{st} (k) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
193		xpopth	$⊢ (1^{st} (z) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land 1^{st} (k) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})) \to ((1^{st} (1^{st} (z)) = 1^{st} (1^{st} (k)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (k))) \leftrightarrow 1^{st} (z) = 1^{st} (k))$
194	191 192 193	syl2an	$⊢ (z \in S \land k \in S) \to ((1^{st} (1^{st} (z)) = 1^{st} (1^{st} (k)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (k))) \leftrightarrow 1^{st} (z) = 1^{st} (k))$
195	194	ad2antlr	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to ((1^{st} (1^{st} (z)) = 1^{st} (1^{st} (k)) \land 2^{nd} (1^{st} (z)) = 2^{nd} (1^{st} (k))) \leftrightarrow 1^{st} (z) = 1^{st} (k))$
196	18 190 195	mpbi2and	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to 1^{st} (z) = 1^{st} (k)$
197		eqtr3	$⊢ (2^{nd} (z) = N \land 2^{nd} (k) = N) \to 2^{nd} (z) = 2^{nd} (k)$
198	197	adantl	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to 2^{nd} (z) = 2^{nd} (k)$
199		xpopth	$⊢ (z \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \land k \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))) \to ((1^{st} (z) = 1^{st} (k) \land 2^{nd} (z) = 2^{nd} (k)) \leftrightarrow z = k)$
200	20 33 199	syl2an	$⊢ (z \in S \land k \in S) \to ((1^{st} (z) = 1^{st} (k) \land 2^{nd} (z) = 2^{nd} (k)) \leftrightarrow z = k)$
201	200	ad2antlr	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to ((1^{st} (z) = 1^{st} (k) \land 2^{nd} (z) = 2^{nd} (k)) \leftrightarrow z = k)$
202	196 198 201	mpbi2and	$⊢ ((φ \land (z \in S \land k \in S)) \land (2^{nd} (z) = N \land 2^{nd} (k) = N)) \to z = k$
203	202	ex	$⊢ (φ \land (z \in S \land k \in S)) \to ((2^{nd} (z) = N \land 2^{nd} (k) = N) \to z = k)$
204	203	ralrimivva	$⊢ φ \to \forall z \in S \forall k \in S ((2^{nd} (z) = N \land 2^{nd} (k) = N) \to z = k)$
205		fveqeq2	$⊢ z = k \to (2^{nd} (z) = N \leftrightarrow 2^{nd} (k) = N)$
206	205	rmo4	$⊢ \exists^{*} z \in S 2^{nd} (z) = N \leftrightarrow \forall z \in S \forall k \in S ((2^{nd} (z) = N \land 2^{nd} (k) = N) \to z = k)$
207	204 206	sylibr	$⊢ φ \to \exists^{*} z \in S 2^{nd} (z) = N$

Metamath Proof Explorer

Theorem poimirlem14

Proof