poimirlem1

Description: Lemma for poimir - the vertices on either side of a skipped vertex differ in at least two dimensions. (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	poimir.0	$⊢ φ \to N \in ℕ$
	poimirlem2.1	$⊢ φ \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < M, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))))$
	poimirlem2.2	$⊢ φ \to T : (1 \dots N) ⟶ ℤ$
	poimirlem2.3	$⊢ φ \to U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
	poimirlem1.4	$⊢ φ \to M \in (1 \dots N - 1)$
Assertion	poimirlem1	$⊢ φ \to \neg \exists^{*} n \in (1 \dots N) F (M - 1) (n) \neq F (M) (n)$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$⊢ φ \to N \in ℕ$
2		poimirlem2.1	$⊢ φ \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < M, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))))$
3		poimirlem2.2	$⊢ φ \to T : (1 \dots N) ⟶ ℤ$
4		poimirlem2.3	$⊢ φ \to U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
5		poimirlem1.4	$⊢ φ \to M \in (1 \dots N - 1)$
6		f1of	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to U : (1 \dots N) ⟶ (1 \dots N)$
7	4 6	syl	$⊢ φ \to U : (1 \dots N) ⟶ (1 \dots N)$
8	1	nncnd	$⊢ φ \to N \in ℂ$
9		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
10	8 9	syl	$⊢ φ \to N - 1 + 1 = N$
11	1	nnzd	$⊢ φ \to N \in ℤ$
12		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
13		uzid	$⊢ N - 1 \in ℤ \to N - 1 \in ℤ_{\geq (N - 1)}$
14		peano2uz	$⊢ N - 1 \in ℤ_{\geq (N - 1)} \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
15	11 12 13 14	4syl	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
16	10 15	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq (N - 1)}$
17		fzss2	$⊢ N \in ℤ_{\geq (N - 1)} \to (1 \dots N - 1) \subseteq (1 \dots N)$
18	16 17	syl	$⊢ φ \to (1 \dots N - 1) \subseteq (1 \dots N)$
19	18 5	sseldd	$⊢ φ \to M \in (1 \dots N)$
20	7 19	ffvelcdmd	$⊢ φ \to U (M) \in (1 \dots N)$
21		fzp1elp1	$⊢ M \in (1 \dots N - 1) \to M + 1 \in (1 \dots N - 1 + 1)$
22	5 21	syl	$⊢ φ \to M + 1 \in (1 \dots N - 1 + 1)$
23	10	oveq2d	$⊢ φ \to (1 \dots N - 1 + 1) = (1 \dots N)$
24	22 23	eleqtrd	$⊢ φ \to M + 1 \in (1 \dots N)$
25	7 24	ffvelcdmd	$⊢ φ \to U (M + 1) \in (1 \dots N)$
26		imassrn	$⊢ U [(M \dots M + 1)] \subseteq ran U$
27		frn	$⊢ U : (1 \dots N) ⟶ (1 \dots N) \to ran U \subseteq (1 \dots N)$
28	4 6 27	3syl	$⊢ φ \to ran U \subseteq (1 \dots N)$
29	26 28	sstrid	$⊢ φ \to U [(M \dots M + 1)] \subseteq (1 \dots N)$
30	29	sselda	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to n \in (1 \dots N)$
31	3	ffvelcdmda	$⊢ (φ \land n \in (1 \dots N)) \to T (n) \in ℤ$
32	31	zred	$⊢ (φ \land n \in (1 \dots N)) \to T (n) \in ℝ$
33	32	ltp1d	$⊢ (φ \land n \in (1 \dots N)) \to T (n) < T (n) + 1$
34	32 33	ltned	$⊢ (φ \land n \in (1 \dots N)) \to T (n) \neq T (n) + 1$
35	30 34	syldan	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to T (n) \neq T (n) + 1$
36		breq1	$⊢ y = M - 1 \to (y < M \leftrightarrow M - 1 < M)$
37		id	$⊢ y = M - 1 \to y = M - 1$
38	36 37	ifbieq1d	$⊢ y = M - 1 \to if (y < M, y, y + 1) = if (M - 1 < M, M - 1, y + 1)$
39		elfzelz	$⊢ M \in (1 \dots N - 1) \to M \in ℤ$
40	5 39	syl	$⊢ φ \to M \in ℤ$
41	40	zred	$⊢ φ \to M \in ℝ$
42	41	ltm1d	$⊢ φ \to M - 1 < M$
43	42	iftrued	$⊢ φ \to if (M - 1 < M, M - 1, y + 1) = M - 1$
44	38 43	sylan9eqr	$⊢ (φ \land y = M - 1) \to if (y < M, y, y + 1) = M - 1$
45	44	csbeq1d	$⊢ (φ \land y = M - 1) \to ⦋ if (y < M, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) = ⦋ (M - 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))$
46	11 12	syl	$⊢ φ \to N - 1 \in ℤ$
47		elfzm1b	$⊢ (M \in ℤ \land N - 1 \in ℤ) \to (M \in (1 \dots N - 1) \leftrightarrow M - 1 \in (0 \dots N - 1 - 1))$
48	40 46 47	syl2anc	$⊢ φ \to (M \in (1 \dots N - 1) \leftrightarrow M - 1 \in (0 \dots N - 1 - 1))$
49	5 48	mpbid	$⊢ φ \to M - 1 \in (0 \dots N - 1 - 1)$
50		oveq2	$⊢ j = M - 1 \to (1 \dots j) = (1 \dots M - 1)$
51	50	imaeq2d	$⊢ j = M - 1 \to U [(1 \dots j)] = U [(1 \dots M - 1)]$
52	51	xpeq1d	$⊢ j = M - 1 \to U [(1 \dots j)] \times \{1\} = U [(1 \dots M - 1)] \times \{1\}$
53	52	adantl	$⊢ (φ \land j = M - 1) \to U [(1 \dots j)] \times \{1\} = U [(1 \dots M - 1)] \times \{1\}$
54		oveq1	$⊢ j = M - 1 \to j + 1 = M - 1 + 1$
55	40	zcnd	$⊢ φ \to M \in ℂ$
56		npcan1	$⊢ M \in ℂ \to M - 1 + 1 = M$
57	55 56	syl	$⊢ φ \to M - 1 + 1 = M$
58	54 57	sylan9eqr	$⊢ (φ \land j = M - 1) \to j + 1 = M$
59	58	oveq1d	$⊢ (φ \land j = M - 1) \to (j + 1 \dots N) = (M \dots N)$
60	59	imaeq2d	$⊢ (φ \land j = M - 1) \to U [(j + 1 \dots N)] = U [(M \dots N)]$
61	60	xpeq1d	$⊢ (φ \land j = M - 1) \to U [(j + 1 \dots N)] \times \{0\} = U [(M \dots N)] \times \{0\}$
62	53 61	uneq12d	$⊢ (φ \land j = M - 1) \to (U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}) = (U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\})$
63	62	oveq2d	$⊢ (φ \land j = M - 1) \to T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) = T +_{f} ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\}))$
64	49 63	csbied	$⊢ φ \to ⦋ (M - 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) = T +_{f} ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\}))$
65	64	adantr	$⊢ (φ \land y = M - 1) \to ⦋ (M - 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) = T +_{f} ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\}))$
66	45 65	eqtrd	$⊢ (φ \land y = M - 1) \to ⦋ if (y < M, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) = T +_{f} ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\}))$
67	46	zcnd	$⊢ φ \to N - 1 \in ℂ$
68		npcan1	$⊢ N - 1 \in ℂ \to (N - 1) - 1 + 1 = N - 1$
69	67 68	syl	$⊢ φ \to (N - 1) - 1 + 1 = N - 1$
70		peano2zm	$⊢ N - 1 \in ℤ \to N - 1 - 1 \in ℤ$
71		uzid	$⊢ N - 1 - 1 \in ℤ \to N - 1 - 1 \in ℤ_{\geq (N - 1 - 1)}$
72		peano2uz	$⊢ N - 1 - 1 \in ℤ_{\geq (N - 1 - 1)} \to (N - 1) - 1 + 1 \in ℤ_{\geq (N - 1 - 1)}$
73	46 70 71 72	4syl	$⊢ φ \to (N - 1) - 1 + 1 \in ℤ_{\geq (N - 1 - 1)}$
74	69 73	eqeltrrd	$⊢ φ \to N - 1 \in ℤ_{\geq (N - 1 - 1)}$
75		fzss2	$⊢ N - 1 \in ℤ_{\geq (N - 1 - 1)} \to (0 \dots N - 1 - 1) \subseteq (0 \dots N - 1)$
76	74 75	syl	$⊢ φ \to (0 \dots N - 1 - 1) \subseteq (0 \dots N - 1)$
77	76 49	sseldd	$⊢ φ \to M - 1 \in (0 \dots N - 1)$
78		ovexd	$⊢ φ \to T +_{f} ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\})) \in V$
79	2 66 77 78	fvmptd	$⊢ φ \to F (M - 1) = T +_{f} ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\}))$
80	79	fveq1d	$⊢ φ \to F (M - 1) (n) = (T +_{f} ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\}))) (n)$
81	80	adantr	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to F (M - 1) (n) = (T +_{f} ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\}))) (n)$
82	3	ffnd	$⊢ φ \to T Fn (1 \dots N)$
83	82	adantr	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to T Fn (1 \dots N)$
84		1ex	$⊢ 1 \in V$
85		fnconstg	$⊢ 1 \in V \to (U [(1 \dots M - 1)] \times \{1\}) Fn U [(1 \dots M - 1)]$
86	84 85	ax-mp	$⊢ (U [(1 \dots M - 1)] \times \{1\}) Fn U [(1 \dots M - 1)]$
87		c0ex	$⊢ 0 \in V$
88		fnconstg	$⊢ 0 \in V \to (U [(M \dots N)] \times \{0\}) Fn U [(M \dots N)]$
89	87 88	ax-mp	$⊢ (U [(M \dots N)] \times \{0\}) Fn U [(M \dots N)]$
90	86 89	pm3.2i	$⊢ ((U [(1 \dots M - 1)] \times \{1\}) Fn U [(1 \dots M - 1)] \land (U [(M \dots N)] \times \{0\}) Fn U [(M \dots N)])$
91		dff1o3	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow (U : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \land Fun U^{-1})$
92	91	simprbi	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun U^{-1}$
93		imain	$⊢ Fun U^{-1} \to U [(1 \dots M - 1) \cap (M \dots N)] = U [(1 \dots M - 1)] \cap U [(M \dots N)]$
94	4 92 93	3syl	$⊢ φ \to U [(1 \dots M - 1) \cap (M \dots N)] = U [(1 \dots M - 1)] \cap U [(M \dots N)]$
95		fzdisj	$⊢ M - 1 < M \to (1 \dots M - 1) \cap (M \dots N) = \emptyset$
96	42 95	syl	$⊢ φ \to (1 \dots M - 1) \cap (M \dots N) = \emptyset$
97	96	imaeq2d	$⊢ φ \to U [(1 \dots M - 1) \cap (M \dots N)] = U [\emptyset]$
98		ima0	$⊢ U [\emptyset] = \emptyset$
99	97 98	eqtrdi	$⊢ φ \to U [(1 \dots M - 1) \cap (M \dots N)] = \emptyset$
100	94 99	eqtr3d	$⊢ φ \to U [(1 \dots M - 1)] \cap U [(M \dots N)] = \emptyset$
101		fnun	$⊢ (((U [(1 \dots M - 1)] \times \{1\}) Fn U [(1 \dots M - 1)] \land (U [(M \dots N)] \times \{0\}) Fn U [(M \dots N)]) \land U [(1 \dots M - 1)] \cap U [(M \dots N)] = \emptyset) \to ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\})) Fn (U [(1 \dots M - 1)] \cup U [(M \dots N)])$
102	90 100 101	sylancr	$⊢ φ \to ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\})) Fn (U [(1 \dots M - 1)] \cup U [(M \dots N)])$
103		elfzuz	$⊢ M \in (1 \dots N - 1) \to M \in ℤ_{\geq 1}$
104	5 103	syl	$⊢ φ \to M \in ℤ_{\geq 1}$
105	57 104	eqeltrd	$⊢ φ \to M - 1 + 1 \in ℤ_{\geq 1}$
106		peano2zm	$⊢ M \in ℤ \to M - 1 \in ℤ$
107		uzid	$⊢ M - 1 \in ℤ \to M - 1 \in ℤ_{\geq (M - 1)}$
108		peano2uz	$⊢ M - 1 \in ℤ_{\geq (M - 1)} \to M - 1 + 1 \in ℤ_{\geq (M - 1)}$
109	40 106 107 108	4syl	$⊢ φ \to M - 1 + 1 \in ℤ_{\geq (M - 1)}$
110	57 109	eqeltrrd	$⊢ φ \to M \in ℤ_{\geq (M - 1)}$
111		peano2uz	$⊢ M \in ℤ_{\geq (M - 1)} \to M + 1 \in ℤ_{\geq (M - 1)}$
112		uzss	$⊢ M + 1 \in ℤ_{\geq (M - 1)} \to ℤ_{\geq (M + 1)} \subseteq ℤ_{\geq (M - 1)}$
113	110 111 112	3syl	$⊢ φ \to ℤ_{\geq (M + 1)} \subseteq ℤ_{\geq (M - 1)}$
114		elfzuz3	$⊢ M \in (1 \dots N - 1) \to N - 1 \in ℤ_{\geq M}$
115		eluzp1p1	$⊢ N - 1 \in ℤ_{\geq M} \to N - 1 + 1 \in ℤ_{\geq (M + 1)}$
116	5 114 115	3syl	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq (M + 1)}$
117	10 116	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq (M + 1)}$
118	113 117	sseldd	$⊢ φ \to N \in ℤ_{\geq (M - 1)}$
119		fzsplit2	$⊢ (M - 1 + 1 \in ℤ_{\geq 1} \land N \in ℤ_{\geq (M - 1)}) \to (1 \dots N) = (1 \dots M - 1) \cup (M - 1 + 1 \dots N)$
120	105 118 119	syl2anc	$⊢ φ \to (1 \dots N) = (1 \dots M - 1) \cup (M - 1 + 1 \dots N)$
121	57	oveq1d	$⊢ φ \to (M - 1 + 1 \dots N) = (M \dots N)$
122	121	uneq2d	$⊢ φ \to (1 \dots M - 1) \cup (M - 1 + 1 \dots N) = (1 \dots M - 1) \cup (M \dots N)$
123	120 122	eqtrd	$⊢ φ \to (1 \dots N) = (1 \dots M - 1) \cup (M \dots N)$
124	123	imaeq2d	$⊢ φ \to U [(1 \dots N)] = U [(1 \dots M - 1) \cup (M \dots N)]$
125		imaundi	$⊢ U [(1 \dots M - 1) \cup (M \dots N)] = U [(1 \dots M - 1)] \cup U [(M \dots N)]$
126	124 125	eqtrdi	$⊢ φ \to U [(1 \dots N)] = U [(1 \dots M - 1)] \cup U [(M \dots N)]$
127		f1ofo	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to U : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
128		foima	$⊢ U : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to U [(1 \dots N)] = (1 \dots N)$
129	4 127 128	3syl	$⊢ φ \to U [(1 \dots N)] = (1 \dots N)$
130	126 129	eqtr3d	$⊢ φ \to U [(1 \dots M - 1)] \cup U [(M \dots N)] = (1 \dots N)$
131	130	fneq2d	$⊢ φ \to (((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\})) Fn (U [(1 \dots M - 1)] \cup U [(M \dots N)]) \leftrightarrow ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\})) Fn (1 \dots N))$
132	102 131	mpbid	$⊢ φ \to ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\})) Fn (1 \dots N)$
133	132	adantr	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\})) Fn (1 \dots N)$
134		ovexd	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to (1 \dots N) \in V$
135		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
136		eqidd	$⊢ ((φ \land n \in U [(M \dots M + 1)]) \land n \in (1 \dots N)) \to T (n) = T (n)$
137	100	adantr	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to U [(1 \dots M - 1)] \cap U [(M \dots N)] = \emptyset$
138		fzss2	$⊢ N \in ℤ_{\geq (M + 1)} \to (M \dots M + 1) \subseteq (M \dots N)$
139		imass2	$⊢ (M \dots M + 1) \subseteq (M \dots N) \to U [(M \dots M + 1)] \subseteq U [(M \dots N)]$
140	117 138 139	3syl	$⊢ φ \to U [(M \dots M + 1)] \subseteq U [(M \dots N)]$
141	140	sselda	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to n \in U [(M \dots N)]$
142		fvun2	$⊢ ((U [(1 \dots M - 1)] \times \{1\}) Fn U [(1 \dots M - 1)] \land (U [(M \dots N)] \times \{0\}) Fn U [(M \dots N)] \land (U [(1 \dots M - 1)] \cap U [(M \dots N)] = \emptyset \land n \in U [(M \dots N)])) \to ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\})) (n) = (U [(M \dots N)] \times \{0\}) (n)$
143	86 89 142	mp3an12	$⊢ (U [(1 \dots M - 1)] \cap U [(M \dots N)] = \emptyset \land n \in U [(M \dots N)]) \to ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\})) (n) = (U [(M \dots N)] \times \{0\}) (n)$
144	137 141 143	syl2anc	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\})) (n) = (U [(M \dots N)] \times \{0\}) (n)$
145	87	fvconst2	$⊢ n \in U [(M \dots N)] \to (U [(M \dots N)] \times \{0\}) (n) = 0$
146	141 145	syl	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to (U [(M \dots N)] \times \{0\}) (n) = 0$
147	144 146	eqtrd	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\})) (n) = 0$
148	147	adantr	$⊢ ((φ \land n \in U [(M \dots M + 1)]) \land n \in (1 \dots N)) \to ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\})) (n) = 0$
149	83 133 134 134 135 136 148	ofval	$⊢ ((φ \land n \in U [(M \dots M + 1)]) \land n \in (1 \dots N)) \to (T +_{f} ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\}))) (n) = T (n) + 0$
150	30 149	mpdan	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to (T +_{f} ((U [(1 \dots M - 1)] \times \{1\}) \cup (U [(M \dots N)] \times \{0\}))) (n) = T (n) + 0$
151	31	zcnd	$⊢ (φ \land n \in (1 \dots N)) \to T (n) \in ℂ$
152	151	addridd	$⊢ (φ \land n \in (1 \dots N)) \to T (n) + 0 = T (n)$
153	30 152	syldan	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to T (n) + 0 = T (n)$
154	81 150 153	3eqtrd	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to F (M - 1) (n) = T (n)$
155		breq1	$⊢ y = M \to (y < M \leftrightarrow M < M)$
156		oveq1	$⊢ y = M \to y + 1 = M + 1$
157	155 156	ifbieq2d	$⊢ y = M \to if (y < M, y, y + 1) = if (M < M, y, M + 1)$
158	41	ltnrd	$⊢ φ \to \neg M < M$
159	158	iffalsed	$⊢ φ \to if (M < M, y, M + 1) = M + 1$
160	157 159	sylan9eqr	$⊢ (φ \land y = M) \to if (y < M, y, y + 1) = M + 1$
161	160	csbeq1d	$⊢ (φ \land y = M) \to ⦋ if (y < M, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) = ⦋ (M + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})))$
162		ovex	$⊢ M + 1 \in V$
163		oveq2	$⊢ j = M + 1 \to (1 \dots j) = (1 \dots M + 1)$
164	163	imaeq2d	$⊢ j = M + 1 \to U [(1 \dots j)] = U [(1 \dots M + 1)]$
165	164	xpeq1d	$⊢ j = M + 1 \to U [(1 \dots j)] \times \{1\} = U [(1 \dots M + 1)] \times \{1\}$
166		oveq1	$⊢ j = M + 1 \to j + 1 = M + 1 + 1$
167	166	oveq1d	$⊢ j = M + 1 \to (j + 1 \dots N) = (M + 1 + 1 \dots N)$
168	167	imaeq2d	$⊢ j = M + 1 \to U [(j + 1 \dots N)] = U [(M + 1 + 1 \dots N)]$
169	168	xpeq1d	$⊢ j = M + 1 \to U [(j + 1 \dots N)] \times \{0\} = U [(M + 1 + 1 \dots N)] \times \{0\}$
170	165 169	uneq12d	$⊢ j = M + 1 \to (U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}) = (U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\})$
171	170	oveq2d	$⊢ j = M + 1 \to T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) = T +_{f} ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\}))$
172	162 171	csbie	$⊢ ⦋ (M + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) = T +_{f} ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\}))$
173	161 172	eqtrdi	$⊢ (φ \land y = M) \to ⦋ if (y < M, y, y + 1) / j ⦌ (T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}))) = T +_{f} ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\}))$
174		fz1ssfz0	$⊢ (1 \dots N - 1) \subseteq (0 \dots N - 1)$
175	174 5	sselid	$⊢ φ \to M \in (0 \dots N - 1)$
176		ovexd	$⊢ φ \to T +_{f} ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\})) \in V$
177	2 173 175 176	fvmptd	$⊢ φ \to F (M) = T +_{f} ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\}))$
178	177	fveq1d	$⊢ φ \to F (M) (n) = (T +_{f} ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\}))) (n)$
179	178	adantr	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to F (M) (n) = (T +_{f} ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\}))) (n)$
180		fnconstg	$⊢ 1 \in V \to (U [(1 \dots M + 1)] \times \{1\}) Fn U [(1 \dots M + 1)]$
181	84 180	ax-mp	$⊢ (U [(1 \dots M + 1)] \times \{1\}) Fn U [(1 \dots M + 1)]$
182		fnconstg	$⊢ 0 \in V \to (U [(M + 1 + 1 \dots N)] \times \{0\}) Fn U [(M + 1 + 1 \dots N)]$
183	87 182	ax-mp	$⊢ (U [(M + 1 + 1 \dots N)] \times \{0\}) Fn U [(M + 1 + 1 \dots N)]$
184	181 183	pm3.2i	$⊢ ((U [(1 \dots M + 1)] \times \{1\}) Fn U [(1 \dots M + 1)] \land (U [(M + 1 + 1 \dots N)] \times \{0\}) Fn U [(M + 1 + 1 \dots N)])$
185		imain	$⊢ Fun U^{-1} \to U [(1 \dots M + 1) \cap (M + 1 + 1 \dots N)] = U [(1 \dots M + 1)] \cap U [(M + 1 + 1 \dots N)]$
186	4 92 185	3syl	$⊢ φ \to U [(1 \dots M + 1) \cap (M + 1 + 1 \dots N)] = U [(1 \dots M + 1)] \cap U [(M + 1 + 1 \dots N)]$
187		peano2re	$⊢ M \in ℝ \to M + 1 \in ℝ$
188	41 187	syl	$⊢ φ \to M + 1 \in ℝ$
189	188	ltp1d	$⊢ φ \to M + 1 < M + 1 + 1$
190		fzdisj	$⊢ M + 1 < M + 1 + 1 \to (1 \dots M + 1) \cap (M + 1 + 1 \dots N) = \emptyset$
191	189 190	syl	$⊢ φ \to (1 \dots M + 1) \cap (M + 1 + 1 \dots N) = \emptyset$
192	191	imaeq2d	$⊢ φ \to U [(1 \dots M + 1) \cap (M + 1 + 1 \dots N)] = U [\emptyset]$
193	186 192	eqtr3d	$⊢ φ \to U [(1 \dots M + 1)] \cap U [(M + 1 + 1 \dots N)] = U [\emptyset]$
194	193 98	eqtrdi	$⊢ φ \to U [(1 \dots M + 1)] \cap U [(M + 1 + 1 \dots N)] = \emptyset$
195		fnun	$⊢ (((U [(1 \dots M + 1)] \times \{1\}) Fn U [(1 \dots M + 1)] \land (U [(M + 1 + 1 \dots N)] \times \{0\}) Fn U [(M + 1 + 1 \dots N)]) \land U [(1 \dots M + 1)] \cap U [(M + 1 + 1 \dots N)] = \emptyset) \to ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\})) Fn (U [(1 \dots M + 1)] \cup U [(M + 1 + 1 \dots N)])$
196	184 194 195	sylancr	$⊢ φ \to ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\})) Fn (U [(1 \dots M + 1)] \cup U [(M + 1 + 1 \dots N)])$
197		fzsplit	$⊢ M + 1 \in (1 \dots N) \to (1 \dots N) = (1 \dots M + 1) \cup (M + 1 + 1 \dots N)$
198	24 197	syl	$⊢ φ \to (1 \dots N) = (1 \dots M + 1) \cup (M + 1 + 1 \dots N)$
199	198	imaeq2d	$⊢ φ \to U [(1 \dots N)] = U [(1 \dots M + 1) \cup (M + 1 + 1 \dots N)]$
200		imaundi	$⊢ U [(1 \dots M + 1) \cup (M + 1 + 1 \dots N)] = U [(1 \dots M + 1)] \cup U [(M + 1 + 1 \dots N)]$
201	199 200	eqtrdi	$⊢ φ \to U [(1 \dots N)] = U [(1 \dots M + 1)] \cup U [(M + 1 + 1 \dots N)]$
202	201 129	eqtr3d	$⊢ φ \to U [(1 \dots M + 1)] \cup U [(M + 1 + 1 \dots N)] = (1 \dots N)$
203	202	fneq2d	$⊢ φ \to (((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\})) Fn (U [(1 \dots M + 1)] \cup U [(M + 1 + 1 \dots N)]) \leftrightarrow ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\})) Fn (1 \dots N))$
204	196 203	mpbid	$⊢ φ \to ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
205	204	adantr	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
206	194	adantr	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to U [(1 \dots M + 1)] \cap U [(M + 1 + 1 \dots N)] = \emptyset$
207		fzss1	$⊢ M \in ℤ_{\geq 1} \to (M \dots M + 1) \subseteq (1 \dots M + 1)$
208		imass2	$⊢ (M \dots M + 1) \subseteq (1 \dots M + 1) \to U [(M \dots M + 1)] \subseteq U [(1 \dots M + 1)]$
209	104 207 208	3syl	$⊢ φ \to U [(M \dots M + 1)] \subseteq U [(1 \dots M + 1)]$
210	209	sselda	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to n \in U [(1 \dots M + 1)]$
211		fvun1	$⊢ ((U [(1 \dots M + 1)] \times \{1\}) Fn U [(1 \dots M + 1)] \land (U [(M + 1 + 1 \dots N)] \times \{0\}) Fn U [(M + 1 + 1 \dots N)] \land (U [(1 \dots M + 1)] \cap U [(M + 1 + 1 \dots N)] = \emptyset \land n \in U [(1 \dots M + 1)])) \to ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\})) (n) = (U [(1 \dots M + 1)] \times \{1\}) (n)$
212	181 183 211	mp3an12	$⊢ (U [(1 \dots M + 1)] \cap U [(M + 1 + 1 \dots N)] = \emptyset \land n \in U [(1 \dots M + 1)]) \to ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\})) (n) = (U [(1 \dots M + 1)] \times \{1\}) (n)$
213	206 210 212	syl2anc	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\})) (n) = (U [(1 \dots M + 1)] \times \{1\}) (n)$
214	84	fvconst2	$⊢ n \in U [(1 \dots M + 1)] \to (U [(1 \dots M + 1)] \times \{1\}) (n) = 1$
215	210 214	syl	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to (U [(1 \dots M + 1)] \times \{1\}) (n) = 1$
216	213 215	eqtrd	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\})) (n) = 1$
217	216	adantr	$⊢ ((φ \land n \in U [(M \dots M + 1)]) \land n \in (1 \dots N)) \to ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\})) (n) = 1$
218	83 205 134 134 135 136 217	ofval	$⊢ ((φ \land n \in U [(M \dots M + 1)]) \land n \in (1 \dots N)) \to (T +_{f} ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\}))) (n) = T (n) + 1$
219	30 218	mpdan	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to (T +_{f} ((U [(1 \dots M + 1)] \times \{1\}) \cup (U [(M + 1 + 1 \dots N)] \times \{0\}))) (n) = T (n) + 1$
220	179 219	eqtrd	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to F (M) (n) = T (n) + 1$
221	35 154 220	3netr4d	$⊢ (φ \land n \in U [(M \dots M + 1)]) \to F (M - 1) (n) \neq F (M) (n)$
222	221	ralrimiva	$⊢ φ \to \forall n \in U [(M \dots M + 1)] F (M - 1) (n) \neq F (M) (n)$
223		fzpr	$⊢ M \in ℤ \to (M \dots M + 1) = \{M, M + 1\}$
224	5 39 223	3syl	$⊢ φ \to (M \dots M + 1) = \{M, M + 1\}$
225	224	imaeq2d	$⊢ φ \to U [(M \dots M + 1)] = U [\{M, M + 1\}]$
226		f1ofn	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to U Fn (1 \dots N)$
227	4 226	syl	$⊢ φ \to U Fn (1 \dots N)$
228		fnimapr	$⊢ (U Fn (1 \dots N) \land M \in (1 \dots N) \land M + 1 \in (1 \dots N)) \to U [\{M, M + 1\}] = \{U (M), U (M + 1)\}$
229	227 19 24 228	syl3anc	$⊢ φ \to U [\{M, M + 1\}] = \{U (M), U (M + 1)\}$
230	225 229	eqtrd	$⊢ φ \to U [(M \dots M + 1)] = \{U (M), U (M + 1)\}$
231	222 230	raleqtrdv	$⊢ φ \to \forall n \in \{U (M), U (M + 1)\} F (M - 1) (n) \neq F (M) (n)$
232		fvex	$⊢ U (M) \in V$
233		fvex	$⊢ U (M + 1) \in V$
234		fveq2	$⊢ n = U (M) \to F (M - 1) (n) = F (M - 1) (U (M))$
235		fveq2	$⊢ n = U (M) \to F (M) (n) = F (M) (U (M))$
236	234 235	neeq12d	$⊢ n = U (M) \to (F (M - 1) (n) \neq F (M) (n) \leftrightarrow F (M - 1) (U (M)) \neq F (M) (U (M)))$
237		fveq2	$⊢ n = U (M + 1) \to F (M - 1) (n) = F (M - 1) (U (M + 1))$
238		fveq2	$⊢ n = U (M + 1) \to F (M) (n) = F (M) (U (M + 1))$
239	237 238	neeq12d	$⊢ n = U (M + 1) \to (F (M - 1) (n) \neq F (M) (n) \leftrightarrow F (M - 1) (U (M + 1)) \neq F (M) (U (M + 1)))$
240	232 233 236 239	ralpr	$⊢ \forall n \in \{U (M), U (M + 1)\} F (M - 1) (n) \neq F (M) (n) \leftrightarrow (F (M - 1) (U (M)) \neq F (M) (U (M)) \land F (M - 1) (U (M + 1)) \neq F (M) (U (M + 1)))$
241	231 240	sylib	$⊢ φ \to (F (M - 1) (U (M)) \neq F (M) (U (M)) \land F (M - 1) (U (M + 1)) \neq F (M) (U (M + 1)))$
242	41	ltp1d	$⊢ φ \to M < M + 1$
243	41 242	ltned	$⊢ φ \to M \neq M + 1$
244		f1of1	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to U : (1 \dots N) \underset{1-1}{⟶} (1 \dots N)$
245	4 244	syl	$⊢ φ \to U : (1 \dots N) \underset{1-1}{⟶} (1 \dots N)$
246		f1veqaeq	$⊢ (U : (1 \dots N) \underset{1-1}{⟶} (1 \dots N) \land (M \in (1 \dots N) \land M + 1 \in (1 \dots N))) \to (U (M) = U (M + 1) \to M = M + 1)$
247	245 19 24 246	syl12anc	$⊢ φ \to (U (M) = U (M + 1) \to M = M + 1)$
248	247	necon3d	$⊢ φ \to (M \neq M + 1 \to U (M) \neq U (M + 1))$
249	243 248	mpd	$⊢ φ \to U (M) \neq U (M + 1)$
250	236	anbi1d	$⊢ n = U (M) \to ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \leftrightarrow (F (M - 1) (U (M)) \neq F (M) (U (M)) \land F (M - 1) (m) \neq F (M) (m)))$
251		neeq1	$⊢ n = U (M) \to (n \neq m \leftrightarrow U (M) \neq m)$
252	250 251	anbi12d	$⊢ n = U (M) \to (((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \land n \neq m) \leftrightarrow ((F (M - 1) (U (M)) \neq F (M) (U (M)) \land F (M - 1) (m) \neq F (M) (m)) \land U (M) \neq m))$
253		fveq2	$⊢ m = U (M + 1) \to F (M - 1) (m) = F (M - 1) (U (M + 1))$
254		fveq2	$⊢ m = U (M + 1) \to F (M) (m) = F (M) (U (M + 1))$
255	253 254	neeq12d	$⊢ m = U (M + 1) \to (F (M - 1) (m) \neq F (M) (m) \leftrightarrow F (M - 1) (U (M + 1)) \neq F (M) (U (M + 1)))$
256	255	anbi2d	$⊢ m = U (M + 1) \to ((F (M - 1) (U (M)) \neq F (M) (U (M)) \land F (M - 1) (m) \neq F (M) (m)) \leftrightarrow (F (M - 1) (U (M)) \neq F (M) (U (M)) \land F (M - 1) (U (M + 1)) \neq F (M) (U (M + 1))))$
257		neeq2	$⊢ m = U (M + 1) \to (U (M) \neq m \leftrightarrow U (M) \neq U (M + 1))$
258	256 257	anbi12d	$⊢ m = U (M + 1) \to (((F (M - 1) (U (M)) \neq F (M) (U (M)) \land F (M - 1) (m) \neq F (M) (m)) \land U (M) \neq m) \leftrightarrow ((F (M - 1) (U (M)) \neq F (M) (U (M)) \land F (M - 1) (U (M + 1)) \neq F (M) (U (M + 1))) \land U (M) \neq U (M + 1)))$
259	252 258	rspc2ev	$⊢ (U (M) \in (1 \dots N) \land U (M + 1) \in (1 \dots N) \land ((F (M - 1) (U (M)) \neq F (M) (U (M)) \land F (M - 1) (U (M + 1)) \neq F (M) (U (M + 1))) \land U (M) \neq U (M + 1))) \to \exists n \in (1 \dots N) \exists m \in (1 \dots N) ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \land n \neq m)$
260	20 25 241 249 259	syl112anc	$⊢ φ \to \exists n \in (1 \dots N) \exists m \in (1 \dots N) ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \land n \neq m)$
261		dfrex2	$⊢ \exists n \in (1 \dots N) \exists m \in (1 \dots N) ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \land n \neq m) \leftrightarrow \neg \forall n \in (1 \dots N) \neg \exists m \in (1 \dots N) ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \land n \neq m)$
262		fveq2	$⊢ n = m \to F (M - 1) (n) = F (M - 1) (m)$
263		fveq2	$⊢ n = m \to F (M) (n) = F (M) (m)$
264	262 263	neeq12d	$⊢ n = m \to (F (M - 1) (n) \neq F (M) (n) \leftrightarrow F (M - 1) (m) \neq F (M) (m))$
265	264	rmo4	$⊢ \exists^{*} n \in (1 \dots N) F (M - 1) (n) \neq F (M) (n) \leftrightarrow \forall n \in (1 \dots N) \forall m \in (1 \dots N) ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \to n = m)$
266		dfral2	$⊢ \forall m \in (1 \dots N) ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \to n = m) \leftrightarrow \neg \exists m \in (1 \dots N) \neg ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \to n = m)$
267		df-ne	$⊢ n \neq m \leftrightarrow \neg n = m$
268	267	anbi2i	$⊢ ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \land n \neq m) \leftrightarrow ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \land \neg n = m)$
269		annim	$⊢ ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \land \neg n = m) \leftrightarrow \neg ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \to n = m)$
270	268 269	bitri	$⊢ ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \land n \neq m) \leftrightarrow \neg ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \to n = m)$
271	270	rexbii	$⊢ \exists m \in (1 \dots N) ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \land n \neq m) \leftrightarrow \exists m \in (1 \dots N) \neg ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \to n = m)$
272	266 271	xchbinxr	$⊢ \forall m \in (1 \dots N) ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \to n = m) \leftrightarrow \neg \exists m \in (1 \dots N) ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \land n \neq m)$
273	272	ralbii	$⊢ \forall n \in (1 \dots N) \forall m \in (1 \dots N) ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \to n = m) \leftrightarrow \forall n \in (1 \dots N) \neg \exists m \in (1 \dots N) ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \land n \neq m)$
274	265 273	bitri	$⊢ \exists^{*} n \in (1 \dots N) F (M - 1) (n) \neq F (M) (n) \leftrightarrow \forall n \in (1 \dots N) \neg \exists m \in (1 \dots N) ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \land n \neq m)$
275	261 274	xchbinxr	$⊢ \exists n \in (1 \dots N) \exists m \in (1 \dots N) ((F (M - 1) (n) \neq F (M) (n) \land F (M - 1) (m) \neq F (M) (m)) \land n \neq m) \leftrightarrow \neg \exists^{*} n \in (1 \dots N) F (M - 1) (n) \neq F (M) (n)$
276	260 275	sylib	$⊢ φ \to \neg \exists^{*} n \in (1 \dots N) F (M - 1) (n) \neq F (M) (n)$

Metamath Proof Explorer

Theorem poimirlem1

Proof