poimirlem18

Description: Lemma for poimir stating that, given a face not on a front face of the main cube and a simplex in which it's opposite the first vertex on 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$
	poimirlem18.3	$⊢ (φ \land n \in (1 \dots N)) \to \exists p \in ran F p (n) \neq K$
	poimirlem18.4	$⊢ φ \to 2^{nd} (T) = 0$
Assertion	poimirlem18	$⊢ φ \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		poimirlem18.3	$⊢ (φ \land n \in (1 \dots N)) \to \exists p \in ran F p (n) \neq K$
6		poimirlem18.4	$⊢ φ \to 2^{nd} (T) = 0$
7	1 2 3 4 5 6	poimirlem17	$⊢ φ \to \exists z \in S z \neq T$
8	6	adantr	$⊢ (φ \land z \in S) \to 2^{nd} (T) = 0$
9		0nnn	$⊢ \neg 0 \in ℕ$
10		elfznn	$⊢ 0 \in (1 \dots N - 1) \to 0 \in ℕ$
11	9 10	mto	$⊢ \neg 0 \in (1 \dots N - 1)$
12		eleq1	$⊢ 2^{nd} (z) = 0 \to (2^{nd} (z) \in (1 \dots N - 1) \leftrightarrow 0 \in (1 \dots N - 1))$
13	11 12	mtbiri	$⊢ 2^{nd} (z) = 0 \to \neg 2^{nd} (z) \in (1 \dots N - 1)$
14	13	necon2ai	$⊢ 2^{nd} (z) \in (1 \dots N - 1) \to 2^{nd} (z) \neq 0$
15	1	ad2antrr	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to N \in ℕ$
16		fveq2	$⊢ t = z \to 2^{nd} (t) = 2^{nd} (z)$
17	16	breq2d	$⊢ t = z \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (z))$
18	17	ifbid	$⊢ t = z \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (z), y, y + 1)$
19	18	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\})))$
20		2fveq3	$⊢ t = z \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (z))$
21		2fveq3	$⊢ t = z \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (z))$
22	21	imaeq1d	$⊢ t = z \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (z)) [(1 \dots j)]$
23	22	xpeq1d	$⊢ t = z \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (z)) [(1 \dots j)] \times \{1\}$
24	21	imaeq1d	$⊢ t = z \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (z)) [(j + 1 \dots N)]$
25	24	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\}$
26	23 25	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\})$
27	20 26	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\}))$
28	27	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\})))$
29	19 28	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\})))$
30	29	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\}))))$
31	30	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\})))))$
32	31 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\})))))$
33	32	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\}))))$
34	33	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\}))))$
35		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))$
36	35 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))$
37		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)\})$
38		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)})$
39		elmapi	$⊢ 1^{st} (1^{st} (z)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ (0 ..^K)$
40	36 37 38 39	4syl	$⊢ z \in S \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ (0 ..^K)$
41		elfzoelz	$⊢ n \in (0 ..^K) \to n \in ℤ$
42	41	ssriv	$⊢ (0 ..^K) \subseteq ℤ$
43		fss	$⊢ (1^{st} (1^{st} (z)) : (1 \dots N) ⟶ (0 ..^K) \land (0 ..^K) \subseteq ℤ) \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ ℤ$
44	40 42 43	sylancl	$⊢ z \in S \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ ℤ$
45	44	ad2antlr	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ ℤ$
46	36 37	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		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)\}$
48	46 47	syl	$⊢ z \in S \to 2^{nd} (1^{st} (z)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
49		fvex	$⊢ 2^{nd} (1^{st} (z)) \in V$
50		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))$
51	49 50	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)$
52	48 51	sylib	$⊢ z \in S \to 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
53	52	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)$
54		simpr	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to 2^{nd} (z) \in (1 \dots N - 1)$
55	15 34 45 53 54	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)$
56	1	ad2antrr	$⊢ ((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land 2^{nd} (T) \neq 2^{nd} (z)) \to N \in ℕ$
57		fveq2	$⊢ t = T \to 2^{nd} (t) = 2^{nd} (T)$
58	57	breq2d	$⊢ t = T \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (T))$
59	58	ifbid	$⊢ t = T \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (T), y, y + 1)$
60	59	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\})))$
61		2fveq3	$⊢ t = T \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T))$
62		2fveq3	$⊢ t = T \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T))$
63	62	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots j)]$
64	63	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}$
65	62	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)]$
66	65	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\}$
67	64 66	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\})$
68	61 67	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\}))$
69	68	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\})))$
70	60 69	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\})))$
71	70	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\}))))$
72	71	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\})))))$
73	72 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\})))))$
74	73	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\}))))$
75	4 74	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\}))))$
76	75	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\}))))$
77		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))$
78	77 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))$
79	4 78	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))$
80		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)\})$
81		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)})$
82		elmapi	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
83	79 80 81 82	4syl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
84		fss	$⊢ (1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K) \land (0 ..^K) \subseteq ℤ) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ ℤ$
85	83 42 84	sylancl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ ℤ$
86	85	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) ⟶ ℤ$
87		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)\}$
88	4 78 80 87	4syl	$⊢ φ \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
89		fvex	$⊢ 2^{nd} (1^{st} (T)) \in V$
90		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))$
91	89 90	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)$
92	88 91	sylib	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
93	92	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)$
94		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)$
95		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)$
96	79 95	syl	$⊢ φ \to 2^{nd} (T) \in (0 \dots N)$
97	96	adantr	$⊢ (φ \land 2^{nd} (z) \in (1 \dots N - 1)) \to 2^{nd} (T) \in (0 \dots N)$
98		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))$
99	98	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)\})$
100	97 99	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)\})$
101	56 76 86 93 94 100	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)$
102	101	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))$
103	102	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))$
104	103	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))$
105	55 104	mpd	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to 2^{nd} (T) = 2^{nd} (z)$
106	105	neeq1d	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to (2^{nd} (T) \neq 0 \leftrightarrow 2^{nd} (z) \neq 0)$
107	106	exbiri	$⊢ (φ \land z \in S) \to (2^{nd} (z) \in (1 \dots N - 1) \to (2^{nd} (z) \neq 0 \to 2^{nd} (T) \neq 0))$
108	14 107	mpdi	$⊢ (φ \land z \in S) \to (2^{nd} (z) \in (1 \dots N - 1) \to 2^{nd} (T) \neq 0)$
109	108	necon2bd	$⊢ (φ \land z \in S) \to (2^{nd} (T) = 0 \to \neg 2^{nd} (z) \in (1 \dots N - 1))$
110	8 109	mpd	$⊢ (φ \land z \in S) \to \neg 2^{nd} (z) \in (1 \dots N - 1)$
111		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)$
112	36 111	syl	$⊢ z \in S \to 2^{nd} (z) \in (0 \dots N)$
113	1	nncnd	$⊢ φ \to N \in ℂ$
114		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
115	113 114	syl	$⊢ φ \to N - 1 + 1 = N$
116		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
117	1 116	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
118	115 117	eqeltrd	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq 1}$
119	1	nnzd	$⊢ φ \to N \in ℤ$
120		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
121		uzid	$⊢ N - 1 \in ℤ \to N - 1 \in ℤ_{\geq (N - 1)}$
122		peano2uz	$⊢ N - 1 \in ℤ_{\geq (N - 1)} \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
123	119 120 121 122	4syl	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
124	115 123	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq (N - 1)}$
125		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)$
126	118 124 125	syl2anc	$⊢ φ \to (1 \dots N) = (1 \dots N - 1) \cup (N - 1 + 1 \dots N)$
127	115	oveq1d	$⊢ φ \to (N - 1 + 1 \dots N) = (N \dots N)$
128		fzsn	$⊢ N \in ℤ \to (N \dots N) = \{N\}$
129	119 128	syl	$⊢ φ \to (N \dots N) = \{N\}$
130	127 129	eqtrd	$⊢ φ \to (N - 1 + 1 \dots N) = \{N\}$
131	130	uneq2d	$⊢ φ \to (1 \dots N - 1) \cup (N - 1 + 1 \dots N) = (1 \dots N - 1) \cup \{N\}$
132	126 131	eqtrd	$⊢ φ \to (1 \dots N) = (1 \dots N - 1) \cup \{N\}$
133	132	eleq2d	$⊢ φ \to (2^{nd} (z) \in (1 \dots N) \leftrightarrow 2^{nd} (z) \in ((1 \dots N - 1) \cup \{N\}))$
134	133	notbid	$⊢ φ \to (\neg 2^{nd} (z) \in (1 \dots N) \leftrightarrow \neg 2^{nd} (z) \in ((1 \dots N - 1) \cup \{N\}))$
135		ioran	$⊢ \neg (2^{nd} (z) \in (1 \dots N - 1) \lor 2^{nd} (z) = N) \leftrightarrow (\neg 2^{nd} (z) \in (1 \dots N - 1) \land \neg 2^{nd} (z) = N)$
136		elun	$⊢ 2^{nd} (z) \in ((1 \dots N - 1) \cup \{N\}) \leftrightarrow (2^{nd} (z) \in (1 \dots N - 1) \lor 2^{nd} (z) \in \{N\})$
137		fvex	$⊢ 2^{nd} (z) \in V$
138	137	elsn	$⊢ 2^{nd} (z) \in \{N\} \leftrightarrow 2^{nd} (z) = N$
139	138	orbi2i	$⊢ (2^{nd} (z) \in (1 \dots N - 1) \lor 2^{nd} (z) \in \{N\}) \leftrightarrow (2^{nd} (z) \in (1 \dots N - 1) \lor 2^{nd} (z) = N)$
140	136 139	bitri	$⊢ 2^{nd} (z) \in ((1 \dots N - 1) \cup \{N\}) \leftrightarrow (2^{nd} (z) \in (1 \dots N - 1) \lor 2^{nd} (z) = N)$
141	135 140	xchnxbir	$⊢ \neg 2^{nd} (z) \in ((1 \dots N - 1) \cup \{N\}) \leftrightarrow (\neg 2^{nd} (z) \in (1 \dots N - 1) \land \neg 2^{nd} (z) = N)$
142	134 141	bitrdi	$⊢ φ \to (\neg 2^{nd} (z) \in (1 \dots N) \leftrightarrow (\neg 2^{nd} (z) \in (1 \dots N - 1) \land \neg 2^{nd} (z) = N))$
143	142	anbi2d	$⊢ φ \to ((2^{nd} (z) \in (0 \dots N) \land \neg 2^{nd} (z) \in (1 \dots N)) \leftrightarrow (2^{nd} (z) \in (0 \dots N) \land (\neg 2^{nd} (z) \in (1 \dots N - 1) \land \neg 2^{nd} (z) = N)))$
144	1	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
145		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
146	144 145	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
147		fzpred	$⊢ N \in ℤ_{\geq 0} \to (0 \dots N) = \{0\} \cup (0 + 1 \dots N)$
148	146 147	syl	$⊢ φ \to (0 \dots N) = \{0\} \cup (0 + 1 \dots N)$
149	148	difeq1d	$⊢ φ \to (0 \dots N) ∖ (1 \dots N) = (\{0\} \cup (0 + 1 \dots N)) ∖ (1 \dots N)$
150		difun2	$⊢ (\{0\} \cup (1 \dots N)) ∖ (1 \dots N) = \{0\} ∖ (1 \dots N)$
151		0p1e1	$⊢ 0 + 1 = 1$
152	151	oveq1i	$⊢ (0 + 1 \dots N) = (1 \dots N)$
153	152	uneq2i	$⊢ \{0\} \cup (0 + 1 \dots N) = \{0\} \cup (1 \dots N)$
154	153	difeq1i	$⊢ (\{0\} \cup (0 + 1 \dots N)) ∖ (1 \dots N) = (\{0\} \cup (1 \dots N)) ∖ (1 \dots N)$
155		incom	$⊢ \{0\} \cap (1 \dots N) = (1 \dots N) \cap \{0\}$
156		elfznn	$⊢ 0 \in (1 \dots N) \to 0 \in ℕ$
157	9 156	mto	$⊢ \neg 0 \in (1 \dots N)$
158		disjsn	$⊢ (1 \dots N) \cap \{0\} = \emptyset \leftrightarrow \neg 0 \in (1 \dots N)$
159	157 158	mpbir	$⊢ (1 \dots N) \cap \{0\} = \emptyset$
160	155 159	eqtri	$⊢ \{0\} \cap (1 \dots N) = \emptyset$
161		disj3	$⊢ \{0\} \cap (1 \dots N) = \emptyset \leftrightarrow \{0\} = \{0\} ∖ (1 \dots N)$
162	160 161	mpbi	$⊢ \{0\} = \{0\} ∖ (1 \dots N)$
163	150 154 162	3eqtr4i	$⊢ (\{0\} \cup (0 + 1 \dots N)) ∖ (1 \dots N) = \{0\}$
164	149 163	eqtrdi	$⊢ φ \to (0 \dots N) ∖ (1 \dots N) = \{0\}$
165	164	eleq2d	$⊢ φ \to (2^{nd} (z) \in ((0 \dots N) ∖ (1 \dots N)) \leftrightarrow 2^{nd} (z) \in \{0\})$
166		eldif	$⊢ 2^{nd} (z) \in ((0 \dots N) ∖ (1 \dots N)) \leftrightarrow (2^{nd} (z) \in (0 \dots N) \land \neg 2^{nd} (z) \in (1 \dots N))$
167	137	elsn	$⊢ 2^{nd} (z) \in \{0\} \leftrightarrow 2^{nd} (z) = 0$
168	165 166 167	3bitr3g	$⊢ φ \to ((2^{nd} (z) \in (0 \dots N) \land \neg 2^{nd} (z) \in (1 \dots N)) \leftrightarrow 2^{nd} (z) = 0)$
169	143 168	bitr3d	$⊢ φ \to ((2^{nd} (z) \in (0 \dots N) \land (\neg 2^{nd} (z) \in (1 \dots N - 1) \land \neg 2^{nd} (z) = N)) \leftrightarrow 2^{nd} (z) = 0)$
170	169	biimpd	$⊢ φ \to ((2^{nd} (z) \in (0 \dots N) \land (\neg 2^{nd} (z) \in (1 \dots N - 1) \land \neg 2^{nd} (z) = N)) \to 2^{nd} (z) = 0)$
171	170	expdimp	$⊢ (φ \land 2^{nd} (z) \in (0 \dots N)) \to ((\neg 2^{nd} (z) \in (1 \dots N - 1) \land \neg 2^{nd} (z) = N) \to 2^{nd} (z) = 0)$
172	112 171	sylan2	$⊢ (φ \land z \in S) \to ((\neg 2^{nd} (z) \in (1 \dots N - 1) \land \neg 2^{nd} (z) = N) \to 2^{nd} (z) = 0)$
173	110 172	mpand	$⊢ (φ \land z \in S) \to (\neg 2^{nd} (z) = N \to 2^{nd} (z) = 0)$
174	1 2 3	poimirlem13	$⊢ φ \to \exists^{*} z \in S 2^{nd} (z) = 0$
175		fveqeq2	$⊢ z = s \to (2^{nd} (z) = 0 \leftrightarrow 2^{nd} (s) = 0)$
176	175	rmo4	$⊢ \exists^{*} z \in S 2^{nd} (z) = 0 \leftrightarrow \forall z \in S \forall s \in S ((2^{nd} (z) = 0 \land 2^{nd} (s) = 0) \to z = s)$
177	174 176	sylib	$⊢ φ \to \forall z \in S \forall s \in S ((2^{nd} (z) = 0 \land 2^{nd} (s) = 0) \to z = s)$
178	177	r19.21bi	$⊢ (φ \land z \in S) \to \forall s \in S ((2^{nd} (z) = 0 \land 2^{nd} (s) = 0) \to z = s)$
179	4	adantr	$⊢ (φ \land z \in S) \to T \in S$
180		fveqeq2	$⊢ s = T \to (2^{nd} (s) = 0 \leftrightarrow 2^{nd} (T) = 0)$
181	180	anbi2d	$⊢ s = T \to ((2^{nd} (z) = 0 \land 2^{nd} (s) = 0) \leftrightarrow (2^{nd} (z) = 0 \land 2^{nd} (T) = 0))$
182		eqeq2	$⊢ s = T \to (z = s \leftrightarrow z = T)$
183	181 182	imbi12d	$⊢ s = T \to (((2^{nd} (z) = 0 \land 2^{nd} (s) = 0) \to z = s) \leftrightarrow ((2^{nd} (z) = 0 \land 2^{nd} (T) = 0) \to z = T))$
184	183	rspccv	$⊢ \forall s \in S ((2^{nd} (z) = 0 \land 2^{nd} (s) = 0) \to z = s) \to (T \in S \to ((2^{nd} (z) = 0 \land 2^{nd} (T) = 0) \to z = T))$
185	178 179 184	sylc	$⊢ (φ \land z \in S) \to ((2^{nd} (z) = 0 \land 2^{nd} (T) = 0) \to z = T)$
186	8 185	mpan2d	$⊢ (φ \land z \in S) \to (2^{nd} (z) = 0 \to z = T)$
187	173 186	syld	$⊢ (φ \land z \in S) \to (\neg 2^{nd} (z) = N \to z = T)$
188	187	necon1ad	$⊢ (φ \land z \in S) \to (z \neq T \to 2^{nd} (z) = N)$
189	188	ralrimiva	$⊢ φ \to \forall z \in S (z \neq T \to 2^{nd} (z) = N)$
190	1 2 3	poimirlem14	$⊢ φ \to \exists^{*} z \in S 2^{nd} (z) = N$
191		rmoim	$⊢ \forall z \in S (z \neq T \to 2^{nd} (z) = N) \to (\exists^{} z \in S 2^{nd} (z) = N \to \exists^{} z \in S z \neq T)$
192	189 190 191	sylc	$⊢ φ \to \exists^{*} z \in S z \neq T$
193		reu5	$⊢ \exists! z \in S z \neq T \leftrightarrow (\exists z \in S z \neq T \land \exists^{*} z \in S z \neq T)$
194	7 192 193	sylanbrc	$⊢ φ \to \exists! z \in S z \neq T$

Metamath Proof Explorer

Theorem poimirlem18

Proof