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	$⊢ φ \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	poimirlem13	$⊢ φ \to \exists^{*} z \in S 2^{nd} (z) = 0$

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

Metamath Proof Explorer

Theorem poimirlem13

Proof