poimirlem21

Description: Lemma for poimir stating that, given a face not on a back face of the cube and a simplex in which it's opposite the final point of the walk, there exists exactly one other simplex containing it. (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)}$
	poimirlem22.2	$⊢ φ \to T \in S$
	poimirlem22.3	$⊢ (φ \land n \in (1 \dots N)) \to \exists p \in ran F p (n) \neq 0$
	poimirlem21.4	$⊢ φ \to 2^{nd} (T) = N$
Assertion	poimirlem21	$⊢ φ \to \exists! z \in S z \neq T$

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		poimirlem22.2	$⊢ φ \to T \in S$
5		poimirlem22.3	$⊢ (φ \land n \in (1 \dots N)) \to \exists p \in ran F p (n) \neq 0$
6		poimirlem21.4	$⊢ φ \to 2^{nd} (T) = N$
7	1 2 3 4 5 6	poimirlem20	$⊢ φ \to \exists z \in S z \neq T$
8	6	adantr	$⊢ (φ \land z \in S) \to 2^{nd} (T) = N$
9	1	nnred	$⊢ φ \to N \in ℝ$
10	9	ltm1d	$⊢ φ \to N - 1 < N$
11		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
12	1 11	syl	$⊢ φ \to N - 1 \in ℕ_{0}$
13	12	nn0red	$⊢ φ \to N - 1 \in ℝ$
14	13 9	ltnled	$⊢ φ \to (N - 1 < N \leftrightarrow \neg N \leq N - 1)$
15	10 14	mpbid	$⊢ φ \to \neg N \leq N - 1$
16		elfzle2	$⊢ N \in (1 \dots N - 1) \to N \leq N - 1$
17	15 16	nsyl	$⊢ φ \to \neg N \in (1 \dots N - 1)$
18		eleq1	$⊢ 2^{nd} (z) = N \to (2^{nd} (z) \in (1 \dots N - 1) \leftrightarrow N \in (1 \dots N - 1))$
19	18	notbid	$⊢ 2^{nd} (z) = N \to (\neg 2^{nd} (z) \in (1 \dots N - 1) \leftrightarrow \neg N \in (1 \dots N - 1))$
20	17 19	syl5ibrcom	$⊢ φ \to (2^{nd} (z) = N \to \neg 2^{nd} (z) \in (1 \dots N - 1))$
21	20	necon2ad	$⊢ φ \to (2^{nd} (z) \in (1 \dots N - 1) \to 2^{nd} (z) \neq N)$
22	21	adantr	$⊢ (φ \land z \in S) \to (2^{nd} (z) \in (1 \dots N - 1) \to 2^{nd} (z) \neq N)$
23	1	ad2antrr	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to N \in ℕ$
24		fveq2	$⊢ t = z \to 2^{nd} (t) = 2^{nd} (z)$
25	24	breq2d	$⊢ t = z \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (z))$
26	25	ifbid	$⊢ t = z \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (z), y, y + 1)$
27	26	csbeq1d	$⊢ t = z \to ⦋ 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\}))) = ⦋ if (y < 2^{nd} (z), 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\})))$
28		2fveq3	$⊢ t = z \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (z))$
29		2fveq3	$⊢ t = z \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (z))$
30	29	imaeq1d	$⊢ t = z \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (z)) [(1 \dots j)]$
31	30	xpeq1d	$⊢ t = z \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}$
32	29	imaeq1d	$⊢ t = z \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (z)) [(j + 1 \dots N)]$
33	32	xpeq1d	$⊢ t = z \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}$
34	31 33	uneq12d	$⊢ t = z \to (2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\})$
35	28 34	oveq12d	$⊢ t = z \to 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\})) = 1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}))$
36	35	csbeq2dv	$⊢ t = z \to ⦋ if (y < 2^{nd} (z), 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\}))) = ⦋ if (y < 2^{nd} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\})))$
37	27 36	eqtrd	$⊢ t = z \to ⦋ 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\}))) = ⦋ if (y < 2^{nd} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\})))$
38	37	mpteq2dv	$⊢ t = z \to (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\})))) = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}))))$
39	38	eqeq2d	$⊢ t = z \to (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\})))) \leftrightarrow F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\})))))$
40	39 2	elrab2	$⊢ z \in S \leftrightarrow (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 F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\})))))$
41	40	simprbi	$⊢ z \in S \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}))))$
42	41	ad2antlr	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (z), y, y + 1) / j ⦌ (1^{st} (1^{st} (z)) +_{f} ((2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (z)) [(j + 1 \dots N)] \times \{0\}))))$
43		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))$
44	43 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))$
45		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)\})$
46	44 45	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)\})$
47		xp1st	$⊢ 1^{st} (z) \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)) \in ({(0 ..^K)}^{(1 \dots N)})$
48	46 47	syl	$⊢ z \in S \to 1^{st} (1^{st} (z)) \in ({(0 ..^K)}^{(1 \dots N)})$
49		elmapi	$⊢ 1^{st} (1^{st} (z)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ (0 ..^K)$
50	48 49	syl	$⊢ z \in S \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ (0 ..^K)$
51		elfzoelz	$⊢ n \in (0 ..^K) \to n \in ℤ$
52	51	ssriv	$⊢ (0 ..^K) \subseteq ℤ$
53		fss	$⊢ (1^{st} (1^{st} (z)) : (1 \dots N) ⟶ (0 ..^K) \land (0 ..^K) \subseteq ℤ) \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ ℤ$
54	50 52 53	sylancl	$⊢ z \in S \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ ℤ$
55	54	ad2antlr	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ ℤ$
56		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)\}$
57	46 56	syl	$⊢ z \in S \to 2^{nd} (1^{st} (z)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
58		fvex	$⊢ 2^{nd} (1^{st} (z)) \in V$
59		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))$
60	58 59	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)$
61	57 60	sylib	$⊢ z \in S \to 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
62	61	ad2antlr	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
63		simpr	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to 2^{nd} (z) \in (1 \dots N - 1)$
64	23 42 55 62 63	poimirlem1	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to \neg \exists^{*} n \in (1 \dots N) F (2^{nd} (z) - 1) (n) \neq F (2^{nd} (z)) (n)$
65	1	ad2antrr	$⊢ ((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land 2^{nd} (T) \neq 2^{nd} (z)) \to N \in ℕ$
66		fveq2	$⊢ t = T \to 2^{nd} (t) = 2^{nd} (T)$
67	66	breq2d	$⊢ t = T \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (T))$
68	67	ifbid	$⊢ t = T \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (T), y, y + 1)$
69	68	csbeq1d	$⊢ t = T \to ⦋ 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\}))) = ⦋ 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\})))$
70		2fveq3	$⊢ t = T \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T))$
71		2fveq3	$⊢ t = T \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T))$
72	71	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots j)]$
73	72	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}$
74	71	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)]$
75	74	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}$
76	73 75	uneq12d	$⊢ t = T \to (2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})$
77	70 76	oveq12d	$⊢ t = T \to 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\})) = 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\}))$
78	77	csbeq2dv	$⊢ t = T \to ⦋ 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\}))) = ⦋ 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\})))$
79	69 78	eqtrd	$⊢ t = T \to ⦋ 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\}))) = ⦋ 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\})))$
80	79	mpteq2dv	$⊢ t = T \to (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\})))) = (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\}))))$
81	80	eqeq2d	$⊢ t = T \to (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\})))) \leftrightarrow 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\})))))$
82	81 2	elrab2	$⊢ T \in S \leftrightarrow (T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \land 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\})))))$
83	82	simprbi	$⊢ T \in S \to 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\}))))$
84	4 83	syl	$⊢ φ \to 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\}))))$
85	84	ad2antrr	$⊢ ((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land 2^{nd} (T) \neq 2^{nd} (z)) \to 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\}))))$
86		elrabi	$⊢ T \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 T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
87	86 2	eleq2s	$⊢ T \in S \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
88	4 87	syl	$⊢ φ \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
89		xp1st	$⊢ T \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} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
90	88 89	syl	$⊢ φ \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
91		xp1st	$⊢ 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
92	90 91	syl	$⊢ φ \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
93		elmapi	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
94	92 93	syl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
95		fss	$⊢ (1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K) \land (0 ..^K) \subseteq ℤ) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ ℤ$
96	94 52 95	sylancl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ ℤ$
97	96	ad2antrr	$⊢ ((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land 2^{nd} (T) \neq 2^{nd} (z)) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ ℤ$
98		xp2nd	$⊢ 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
99	90 98	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
100		fvex	$⊢ 2^{nd} (1^{st} (T)) \in V$
101		f1oeq1	$⊢ f = 2^{nd} (1^{st} (T)) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
102	100 101	elab	$⊢ 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
103	99 102	sylib	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
104	103	ad2antrr	$⊢ ((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land 2^{nd} (T) \neq 2^{nd} (z)) \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
105		simplr	$⊢ ((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land 2^{nd} (T) \neq 2^{nd} (z)) \to 2^{nd} (z) \in (1 \dots N - 1)$
106		xp2nd	$⊢ T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \to 2^{nd} (T) \in (0 \dots N)$
107	88 106	syl	$⊢ φ \to 2^{nd} (T) \in (0 \dots N)$
108	107	adantr	$⊢ (φ \land 2^{nd} (z) \in (1 \dots N - 1)) \to 2^{nd} (T) \in (0 \dots N)$
109		eldifsn	$⊢ 2^{nd} (T) \in ((0 \dots N) ∖ \{2^{nd} (z)\}) \leftrightarrow (2^{nd} (T) \in (0 \dots N) \land 2^{nd} (T) \neq 2^{nd} (z))$
110	109	biimpri	$⊢ (2^{nd} (T) \in (0 \dots N) \land 2^{nd} (T) \neq 2^{nd} (z)) \to 2^{nd} (T) \in ((0 \dots N) ∖ \{2^{nd} (z)\})$
111	108 110	sylan	$⊢ ((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land 2^{nd} (T) \neq 2^{nd} (z)) \to 2^{nd} (T) \in ((0 \dots N) ∖ \{2^{nd} (z)\})$
112	65 85 97 104 105 111	poimirlem2	$⊢ ((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land 2^{nd} (T) \neq 2^{nd} (z)) \to \exists^{*} n \in (1 \dots N) F (2^{nd} (z) - 1) (n) \neq F (2^{nd} (z)) (n)$
113	112	ex	$⊢ (φ \land 2^{nd} (z) \in (1 \dots N - 1)) \to (2^{nd} (T) \neq 2^{nd} (z) \to \exists^{*} n \in (1 \dots N) F (2^{nd} (z) - 1) (n) \neq F (2^{nd} (z)) (n))$
114	113	necon1bd	$⊢ (φ \land 2^{nd} (z) \in (1 \dots N - 1)) \to (\neg \exists^{*} n \in (1 \dots N) F (2^{nd} (z) - 1) (n) \neq F (2^{nd} (z)) (n) \to 2^{nd} (T) = 2^{nd} (z))$
115	114	adantlr	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to (\neg \exists^{*} n \in (1 \dots N) F (2^{nd} (z) - 1) (n) \neq F (2^{nd} (z)) (n) \to 2^{nd} (T) = 2^{nd} (z))$
116	64 115	mpd	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to 2^{nd} (T) = 2^{nd} (z)$
117	116	neeq1d	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to (2^{nd} (T) \neq N \leftrightarrow 2^{nd} (z) \neq N)$
118	117	exbiri	$⊢ (φ \land z \in S) \to (2^{nd} (z) \in (1 \dots N - 1) \to (2^{nd} (z) \neq N \to 2^{nd} (T) \neq N))$
119	22 118	mpdd	$⊢ (φ \land z \in S) \to (2^{nd} (z) \in (1 \dots N - 1) \to 2^{nd} (T) \neq N)$
120	119	necon2bd	$⊢ (φ \land z \in S) \to (2^{nd} (T) = N \to \neg 2^{nd} (z) \in (1 \dots N - 1))$
121	8 120	mpd	$⊢ (φ \land z \in S) \to \neg 2^{nd} (z) \in (1 \dots N - 1)$
122		xp2nd	$⊢ 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 2^{nd} (z) \in (0 \dots N)$
123	44 122	syl	$⊢ z \in S \to 2^{nd} (z) \in (0 \dots N)$
124		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
125	12 124	eleqtrdi	$⊢ φ \to N - 1 \in ℤ_{\geq 0}$
126		fzpred	$⊢ N - 1 \in ℤ_{\geq 0} \to (0 \dots N - 1) = \{0\} \cup (0 + 1 \dots N - 1)$
127	125 126	syl	$⊢ φ \to (0 \dots N - 1) = \{0\} \cup (0 + 1 \dots N - 1)$
128		0p1e1	$⊢ 0 + 1 = 1$
129	128	oveq1i	$⊢ (0 + 1 \dots N - 1) = (1 \dots N - 1)$
130	129	uneq2i	$⊢ \{0\} \cup (0 + 1 \dots N - 1) = \{0\} \cup (1 \dots N - 1)$
131	127 130	eqtrdi	$⊢ φ \to (0 \dots N - 1) = \{0\} \cup (1 \dots N - 1)$
132	131	eleq2d	$⊢ φ \to (2^{nd} (z) \in (0 \dots N - 1) \leftrightarrow 2^{nd} (z) \in (\{0\} \cup (1 \dots N - 1)))$
133	132	notbid	$⊢ φ \to (\neg 2^{nd} (z) \in (0 \dots N - 1) \leftrightarrow \neg 2^{nd} (z) \in (\{0\} \cup (1 \dots N - 1)))$
134		ioran	$⊢ \neg (2^{nd} (z) = 0 \lor 2^{nd} (z) \in (1 \dots N - 1)) \leftrightarrow (\neg 2^{nd} (z) = 0 \land \neg 2^{nd} (z) \in (1 \dots N - 1))$
135		elun	$⊢ 2^{nd} (z) \in (\{0\} \cup (1 \dots N - 1)) \leftrightarrow (2^{nd} (z) \in \{0\} \lor 2^{nd} (z) \in (1 \dots N - 1))$
136		fvex	$⊢ 2^{nd} (z) \in V$
137	136	elsn	$⊢ 2^{nd} (z) \in \{0\} \leftrightarrow 2^{nd} (z) = 0$
138	137	orbi1i	$⊢ (2^{nd} (z) \in \{0\} \lor 2^{nd} (z) \in (1 \dots N - 1)) \leftrightarrow (2^{nd} (z) = 0 \lor 2^{nd} (z) \in (1 \dots N - 1))$
139	135 138	bitri	$⊢ 2^{nd} (z) \in (\{0\} \cup (1 \dots N - 1)) \leftrightarrow (2^{nd} (z) = 0 \lor 2^{nd} (z) \in (1 \dots N - 1))$
140	134 139	xchnxbir	$⊢ \neg 2^{nd} (z) \in (\{0\} \cup (1 \dots N - 1)) \leftrightarrow (\neg 2^{nd} (z) = 0 \land \neg 2^{nd} (z) \in (1 \dots N - 1))$
141	133 140	bitrdi	$⊢ φ \to (\neg 2^{nd} (z) \in (0 \dots N - 1) \leftrightarrow (\neg 2^{nd} (z) = 0 \land \neg 2^{nd} (z) \in (1 \dots N - 1)))$
142	141	anbi2d	$⊢ φ \to ((2^{nd} (z) \in (0 \dots N) \land \neg 2^{nd} (z) \in (0 \dots N - 1)) \leftrightarrow (2^{nd} (z) \in (0 \dots N) \land (\neg 2^{nd} (z) = 0 \land \neg 2^{nd} (z) \in (1 \dots N - 1))))$
143		uncom	$⊢ (0 \dots N - 1) \cup \{N\} = \{N\} \cup (0 \dots N - 1)$
144	143	difeq1i	$⊢ ((0 \dots N - 1) \cup \{N\}) ∖ (0 \dots N - 1) = (\{N\} \cup (0 \dots N - 1)) ∖ (0 \dots N - 1)$
145		difun2	$⊢ (\{N\} \cup (0 \dots N - 1)) ∖ (0 \dots N - 1) = \{N\} ∖ (0 \dots N - 1)$
146	144 145	eqtri	$⊢ ((0 \dots N - 1) \cup \{N\}) ∖ (0 \dots N - 1) = \{N\} ∖ (0 \dots N - 1)$
147	1	nncnd	$⊢ φ \to N \in ℂ$
148		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
149	147 148	syl	$⊢ φ \to N - 1 + 1 = N$
150	1	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
151	150 124	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
152	149 151	eqeltrd	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq 0}$
153	12	nn0zd	$⊢ φ \to N - 1 \in ℤ$
154		uzid	$⊢ N - 1 \in ℤ \to N - 1 \in ℤ_{\geq (N - 1)}$
155		peano2uz	$⊢ N - 1 \in ℤ_{\geq (N - 1)} \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
156	153 154 155	3syl	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
157	149 156	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq (N - 1)}$
158		fzsplit2	$⊢ (N - 1 + 1 \in ℤ_{\geq 0} \land N \in ℤ_{\geq (N - 1)}) \to (0 \dots N) = (0 \dots N - 1) \cup (N - 1 + 1 \dots N)$
159	152 157 158	syl2anc	$⊢ φ \to (0 \dots N) = (0 \dots N - 1) \cup (N - 1 + 1 \dots N)$
160	149	oveq1d	$⊢ φ \to (N - 1 + 1 \dots N) = (N \dots N)$
161	1	nnzd	$⊢ φ \to N \in ℤ$
162		fzsn	$⊢ N \in ℤ \to (N \dots N) = \{N\}$
163	161 162	syl	$⊢ φ \to (N \dots N) = \{N\}$
164	160 163	eqtrd	$⊢ φ \to (N - 1 + 1 \dots N) = \{N\}$
165	164	uneq2d	$⊢ φ \to (0 \dots N - 1) \cup (N - 1 + 1 \dots N) = (0 \dots N - 1) \cup \{N\}$
166	159 165	eqtrd	$⊢ φ \to (0 \dots N) = (0 \dots N - 1) \cup \{N\}$
167	166	difeq1d	$⊢ φ \to (0 \dots N) ∖ (0 \dots N - 1) = ((0 \dots N - 1) \cup \{N\}) ∖ (0 \dots N - 1)$
168		elfzle2	$⊢ N \in (0 \dots N - 1) \to N \leq N - 1$
169	15 168	nsyl	$⊢ φ \to \neg N \in (0 \dots N - 1)$
170		incom	$⊢ (0 \dots N - 1) \cap \{N\} = \{N\} \cap (0 \dots N - 1)$
171	170	eqeq1i	$⊢ (0 \dots N - 1) \cap \{N\} = \emptyset \leftrightarrow \{N\} \cap (0 \dots N - 1) = \emptyset$
172		disjsn	$⊢ (0 \dots N - 1) \cap \{N\} = \emptyset \leftrightarrow \neg N \in (0 \dots N - 1)$
173		disj3	$⊢ \{N\} \cap (0 \dots N - 1) = \emptyset \leftrightarrow \{N\} = \{N\} ∖ (0 \dots N - 1)$
174	171 172 173	3bitr3i	$⊢ \neg N \in (0 \dots N - 1) \leftrightarrow \{N\} = \{N\} ∖ (0 \dots N - 1)$
175	169 174	sylib	$⊢ φ \to \{N\} = \{N\} ∖ (0 \dots N - 1)$
176	146 167 175	3eqtr4a	$⊢ φ \to (0 \dots N) ∖ (0 \dots N - 1) = \{N\}$
177	176	eleq2d	$⊢ φ \to (2^{nd} (z) \in ((0 \dots N) ∖ (0 \dots N - 1)) \leftrightarrow 2^{nd} (z) \in \{N\})$
178		eldif	$⊢ 2^{nd} (z) \in ((0 \dots N) ∖ (0 \dots N - 1)) \leftrightarrow (2^{nd} (z) \in (0 \dots N) \land \neg 2^{nd} (z) \in (0 \dots N - 1))$
179	136	elsn	$⊢ 2^{nd} (z) \in \{N\} \leftrightarrow 2^{nd} (z) = N$
180	177 178 179	3bitr3g	$⊢ φ \to ((2^{nd} (z) \in (0 \dots N) \land \neg 2^{nd} (z) \in (0 \dots N - 1)) \leftrightarrow 2^{nd} (z) = N)$
181	142 180	bitr3d	$⊢ φ \to ((2^{nd} (z) \in (0 \dots N) \land (\neg 2^{nd} (z) = 0 \land \neg 2^{nd} (z) \in (1 \dots N - 1))) \leftrightarrow 2^{nd} (z) = N)$
182	181	biimpd	$⊢ φ \to ((2^{nd} (z) \in (0 \dots N) \land (\neg 2^{nd} (z) = 0 \land \neg 2^{nd} (z) \in (1 \dots N - 1))) \to 2^{nd} (z) = N)$
183	182	expdimp	$⊢ (φ \land 2^{nd} (z) \in (0 \dots N)) \to ((\neg 2^{nd} (z) = 0 \land \neg 2^{nd} (z) \in (1 \dots N - 1)) \to 2^{nd} (z) = N)$
184	123 183	sylan2	$⊢ (φ \land z \in S) \to ((\neg 2^{nd} (z) = 0 \land \neg 2^{nd} (z) \in (1 \dots N - 1)) \to 2^{nd} (z) = N)$
185	121 184	mpan2d	$⊢ (φ \land z \in S) \to (\neg 2^{nd} (z) = 0 \to 2^{nd} (z) = N)$
186	1 2 3	poimirlem14	$⊢ φ \to \exists^{*} z \in S 2^{nd} (z) = N$
187		fveqeq2	$⊢ z = s \to (2^{nd} (z) = N \leftrightarrow 2^{nd} (s) = N)$
188	187	rmo4	$⊢ \exists^{*} z \in S 2^{nd} (z) = N \leftrightarrow \forall z \in S \forall s \in S ((2^{nd} (z) = N \land 2^{nd} (s) = N) \to z = s)$
189	186 188	sylib	$⊢ φ \to \forall z \in S \forall s \in S ((2^{nd} (z) = N \land 2^{nd} (s) = N) \to z = s)$
190	189	r19.21bi	$⊢ (φ \land z \in S) \to \forall s \in S ((2^{nd} (z) = N \land 2^{nd} (s) = N) \to z = s)$
191	4	adantr	$⊢ (φ \land z \in S) \to T \in S$
192		fveqeq2	$⊢ s = T \to (2^{nd} (s) = N \leftrightarrow 2^{nd} (T) = N)$
193	192	anbi2d	$⊢ s = T \to ((2^{nd} (z) = N \land 2^{nd} (s) = N) \leftrightarrow (2^{nd} (z) = N \land 2^{nd} (T) = N))$
194		eqeq2	$⊢ s = T \to (z = s \leftrightarrow z = T)$
195	193 194	imbi12d	$⊢ s = T \to (((2^{nd} (z) = N \land 2^{nd} (s) = N) \to z = s) \leftrightarrow ((2^{nd} (z) = N \land 2^{nd} (T) = N) \to z = T))$
196	195	rspccv	$⊢ \forall s \in S ((2^{nd} (z) = N \land 2^{nd} (s) = N) \to z = s) \to (T \in S \to ((2^{nd} (z) = N \land 2^{nd} (T) = N) \to z = T))$
197	190 191 196	sylc	$⊢ (φ \land z \in S) \to ((2^{nd} (z) = N \land 2^{nd} (T) = N) \to z = T)$
198	8 197	mpan2d	$⊢ (φ \land z \in S) \to (2^{nd} (z) = N \to z = T)$
199	185 198	syld	$⊢ (φ \land z \in S) \to (\neg 2^{nd} (z) = 0 \to z = T)$
200	199	necon1ad	$⊢ (φ \land z \in S) \to (z \neq T \to 2^{nd} (z) = 0)$
201	200	ralrimiva	$⊢ φ \to \forall z \in S (z \neq T \to 2^{nd} (z) = 0)$
202	1 2 3	poimirlem13	$⊢ φ \to \exists^{*} z \in S 2^{nd} (z) = 0$
203		rmoim	$⊢ \forall z \in S (z \neq T \to 2^{nd} (z) = 0) \to (\exists^{} z \in S 2^{nd} (z) = 0 \to \exists^{} z \in S z \neq T)$
204	201 202 203	sylc	$⊢ φ \to \exists^{*} z \in S z \neq T$
205		reu5	$⊢ \exists! z \in S z \neq T \leftrightarrow (\exists z \in S z \neq T \land \exists^{*} z \in S z \neq T)$
206	7 204 205	sylanbrc	$⊢ φ \to \exists! z \in S z \neq T$

Metamath Proof Explorer

Theorem poimirlem21

Proof