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	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)\})$
39		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)})$
40	38 39	syl	$⊢ z \in S \to 1^{st} (1^{st} (z)) \in ({(0 ..^K)}^{(1 \dots N)})$
41		elmapi	$⊢ 1^{st} (1^{st} (z)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ (0 ..^K)$
42	40 41	syl	$⊢ z \in S \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ (0 ..^K)$
43		elfzoelz	$⊢ n \in (0 ..^K) \to n \in ℤ$
44	43	ssriv	$⊢ (0 ..^K) \subseteq ℤ$
45		fss	$⊢ (1^{st} (1^{st} (z)) : (1 \dots N) ⟶ (0 ..^K) \land (0 ..^K) \subseteq ℤ) \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ ℤ$
46	42 44 45	sylancl	$⊢ z \in S \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ ℤ$
47	46	ad2antlr	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to 1^{st} (1^{st} (z)) : (1 \dots N) ⟶ ℤ$
48		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)\}$
49	38 48	syl	$⊢ z \in S \to 2^{nd} (1^{st} (z)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
50		fvex	$⊢ 2^{nd} (1^{st} (z)) \in V$
51		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))$
52	50 51	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)$
53	49 52	sylib	$⊢ z \in S \to 2^{nd} (1^{st} (z)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
54	53	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)$
55		simpr	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to 2^{nd} (z) \in (1 \dots N - 1)$
56	15 34 47 54 55	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)$
57	1	ad2antrr	$⊢ ((φ \land 2^{nd} (z) \in (1 \dots N - 1)) \land 2^{nd} (T) \neq 2^{nd} (z)) \to N \in ℕ$
58		fveq2	$⊢ t = T \to 2^{nd} (t) = 2^{nd} (T)$
59	58	breq2d	$⊢ t = T \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (T))$
60	59	ifbid	$⊢ t = T \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (T), y, y + 1)$
61	60	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\})))$
62		2fveq3	$⊢ t = T \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T))$
63		2fveq3	$⊢ t = T \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T))$
64	63	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots j)]$
65	64	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}$
66	63	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)]$
67	66	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\}$
68	65 67	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\})$
69	62 68	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\}))$
70	69	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\})))$
71	61 70	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\})))$
72	71	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\}))))$
73	72	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\})))))$
74	73 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\})))))$
75	74	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\}))))$
76	4 75	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\}))))$
77	76	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\}))))$
78		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))$
79	78 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))$
80	4 79	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))$
81		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)\})$
82	80 81	syl	$⊢ φ \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
83		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)})$
84	82 83	syl	$⊢ φ \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
85		elmapi	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
86	84 85	syl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
87		fss	$⊢ (1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K) \land (0 ..^K) \subseteq ℤ) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ ℤ$
88	86 44 87	sylancl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ ℤ$
89	88	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) ⟶ ℤ$
90		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)\}$
91	82 90	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
92		fvex	$⊢ 2^{nd} (1^{st} (T)) \in V$
93		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))$
94	92 93	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)$
95	91 94	sylib	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
96	95	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)$
97		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)$
98		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)$
99	80 98	syl	$⊢ φ \to 2^{nd} (T) \in (0 \dots N)$
100	99	adantr	$⊢ (φ \land 2^{nd} (z) \in (1 \dots N - 1)) \to 2^{nd} (T) \in (0 \dots N)$
101		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))$
102	101	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)\})$
103	100 102	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)\})$
104	57 77 89 96 97 103	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)$
105	104	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))$
106	105	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))$
107	106	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))$
108	56 107	mpd	$⊢ ((φ \land z \in S) \land 2^{nd} (z) \in (1 \dots N - 1)) \to 2^{nd} (T) = 2^{nd} (z)$
109	108	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)$
110	109	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))$
111	14 110	mpdi	$⊢ (φ \land z \in S) \to (2^{nd} (z) \in (1 \dots N - 1) \to 2^{nd} (T) \neq 0)$
112	111	necon2bd	$⊢ (φ \land z \in S) \to (2^{nd} (T) = 0 \to \neg 2^{nd} (z) \in (1 \dots N - 1))$
113	8 112	mpd	$⊢ (φ \land z \in S) \to \neg 2^{nd} (z) \in (1 \dots N - 1)$
114		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)$
115	36 114	syl	$⊢ z \in S \to 2^{nd} (z) \in (0 \dots N)$
116	1	nncnd	$⊢ φ \to N \in ℂ$
117		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
118	116 117	syl	$⊢ φ \to N - 1 + 1 = N$
119		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
120	1 119	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
121	118 120	eqeltrd	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq 1}$
122	1	nnzd	$⊢ φ \to N \in ℤ$
123		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
124	122 123	syl	$⊢ φ \to N - 1 \in ℤ$
125		uzid	$⊢ N - 1 \in ℤ \to N - 1 \in ℤ_{\geq (N - 1)}$
126		peano2uz	$⊢ N - 1 \in ℤ_{\geq (N - 1)} \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
127	124 125 126	3syl	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
128	118 127	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq (N - 1)}$
129		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)$
130	121 128 129	syl2anc	$⊢ φ \to (1 \dots N) = (1 \dots N - 1) \cup (N - 1 + 1 \dots N)$
131	118	oveq1d	$⊢ φ \to (N - 1 + 1 \dots N) = (N \dots N)$
132		fzsn	$⊢ N \in ℤ \to (N \dots N) = \{N\}$
133	122 132	syl	$⊢ φ \to (N \dots N) = \{N\}$
134	131 133	eqtrd	$⊢ φ \to (N - 1 + 1 \dots N) = \{N\}$
135	134	uneq2d	$⊢ φ \to (1 \dots N - 1) \cup (N - 1 + 1 \dots N) = (1 \dots N - 1) \cup \{N\}$
136	130 135	eqtrd	$⊢ φ \to (1 \dots N) = (1 \dots N - 1) \cup \{N\}$
137	136	eleq2d	$⊢ φ \to (2^{nd} (z) \in (1 \dots N) \leftrightarrow 2^{nd} (z) \in ((1 \dots N - 1) \cup \{N\}))$
138	137	notbid	$⊢ φ \to (\neg 2^{nd} (z) \in (1 \dots N) \leftrightarrow \neg 2^{nd} (z) \in ((1 \dots N - 1) \cup \{N\}))$
139		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)$
140		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\})$
141		fvex	$⊢ 2^{nd} (z) \in V$
142	141	elsn	$⊢ 2^{nd} (z) \in \{N\} \leftrightarrow 2^{nd} (z) = N$
143	142	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)$
144	140 143	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)$
145	139 144	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)$
146	138 145	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))$
147	146	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)))$
148	1	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
149		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
150	148 149	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
151		fzpred	$⊢ N \in ℤ_{\geq 0} \to (0 \dots N) = \{0\} \cup (0 + 1 \dots N)$
152	150 151	syl	$⊢ φ \to (0 \dots N) = \{0\} \cup (0 + 1 \dots N)$
153	152	difeq1d	$⊢ φ \to (0 \dots N) ∖ (1 \dots N) = (\{0\} \cup (0 + 1 \dots N)) ∖ (1 \dots N)$
154		difun2	$⊢ (\{0\} \cup (1 \dots N)) ∖ (1 \dots N) = \{0\} ∖ (1 \dots N)$
155		0p1e1	$⊢ 0 + 1 = 1$
156	155	oveq1i	$⊢ (0 + 1 \dots N) = (1 \dots N)$
157	156	uneq2i	$⊢ \{0\} \cup (0 + 1 \dots N) = \{0\} \cup (1 \dots N)$
158	157	difeq1i	$⊢ (\{0\} \cup (0 + 1 \dots N)) ∖ (1 \dots N) = (\{0\} \cup (1 \dots N)) ∖ (1 \dots N)$
159		incom	$⊢ \{0\} \cap (1 \dots N) = (1 \dots N) \cap \{0\}$
160		elfznn	$⊢ 0 \in (1 \dots N) \to 0 \in ℕ$
161	9 160	mto	$⊢ \neg 0 \in (1 \dots N)$
162		disjsn	$⊢ (1 \dots N) \cap \{0\} = \emptyset \leftrightarrow \neg 0 \in (1 \dots N)$
163	161 162	mpbir	$⊢ (1 \dots N) \cap \{0\} = \emptyset$
164	159 163	eqtri	$⊢ \{0\} \cap (1 \dots N) = \emptyset$
165		disj3	$⊢ \{0\} \cap (1 \dots N) = \emptyset \leftrightarrow \{0\} = \{0\} ∖ (1 \dots N)$
166	164 165	mpbi	$⊢ \{0\} = \{0\} ∖ (1 \dots N)$
167	154 158 166	3eqtr4i	$⊢ (\{0\} \cup (0 + 1 \dots N)) ∖ (1 \dots N) = \{0\}$
168	153 167	eqtrdi	$⊢ φ \to (0 \dots N) ∖ (1 \dots N) = \{0\}$
169	168	eleq2d	$⊢ φ \to (2^{nd} (z) \in ((0 \dots N) ∖ (1 \dots N)) \leftrightarrow 2^{nd} (z) \in \{0\})$
170		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))$
171	141	elsn	$⊢ 2^{nd} (z) \in \{0\} \leftrightarrow 2^{nd} (z) = 0$
172	169 170 171	3bitr3g	$⊢ φ \to ((2^{nd} (z) \in (0 \dots N) \land \neg 2^{nd} (z) \in (1 \dots N)) \leftrightarrow 2^{nd} (z) = 0)$
173	147 172	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)$
174	173	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)$
175	174	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)$
176	115 175	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)$
177	113 176	mpand	$⊢ (φ \land z \in S) \to (\neg 2^{nd} (z) = N \to 2^{nd} (z) = 0)$
178	1 2 3	poimirlem13	$⊢ φ \to \exists^{*} z \in S 2^{nd} (z) = 0$
179		fveqeq2	$⊢ z = s \to (2^{nd} (z) = 0 \leftrightarrow 2^{nd} (s) = 0)$
180	179	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)$
181	178 180	sylib	$⊢ φ \to \forall z \in S \forall s \in S ((2^{nd} (z) = 0 \land 2^{nd} (s) = 0) \to z = s)$
182	181	r19.21bi	$⊢ (φ \land z \in S) \to \forall s \in S ((2^{nd} (z) = 0 \land 2^{nd} (s) = 0) \to z = s)$
183	4	adantr	$⊢ (φ \land z \in S) \to T \in S$
184		fveqeq2	$⊢ s = T \to (2^{nd} (s) = 0 \leftrightarrow 2^{nd} (T) = 0)$
185	184	anbi2d	$⊢ s = T \to ((2^{nd} (z) = 0 \land 2^{nd} (s) = 0) \leftrightarrow (2^{nd} (z) = 0 \land 2^{nd} (T) = 0))$
186		eqeq2	$⊢ s = T \to (z = s \leftrightarrow z = T)$
187	185 186	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))$
188	187	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))$
189	182 183 188	sylc	$⊢ (φ \land z \in S) \to ((2^{nd} (z) = 0 \land 2^{nd} (T) = 0) \to z = T)$
190	8 189	mpan2d	$⊢ (φ \land z \in S) \to (2^{nd} (z) = 0 \to z = T)$
191	177 190	syld	$⊢ (φ \land z \in S) \to (\neg 2^{nd} (z) = N \to z = T)$
192	191	necon1ad	$⊢ (φ \land z \in S) \to (z \neq T \to 2^{nd} (z) = N)$
193	192	ralrimiva	$⊢ φ \to \forall z \in S (z \neq T \to 2^{nd} (z) = N)$
194	1 2 3	poimirlem14	$⊢ φ \to \exists^{*} z \in S 2^{nd} (z) = N$
195		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)$
196	193 194 195	sylc	$⊢ φ \to \exists^{*} z \in S z \neq T$
197		reu5	$⊢ \exists! z \in S z \neq T \leftrightarrow (\exists z \in S z \neq T \land \exists^{*} z \in S z \neq T)$
198	7 196 197	sylanbrc	$⊢ φ \to \exists! z \in S z \neq T$

Metamath Proof Explorer

Theorem poimirlem18

Proof