poimirlem2

Description: Lemma for poimir - consecutive vertices differ in at most one dimension. (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)$
	poimirlem2.4	$⊢ φ \to V \in (1 \dots N - 1)$
	poimirlem2.5	$⊢ φ \to M \in ((0 \dots N) ∖ \{V\})$
Assertion	poimirlem2	$⊢ φ \to \exists^{*} n \in (1 \dots N) F (V - 1) (n) \neq F (V) (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		poimirlem2.4	$⊢ φ \to V \in (1 \dots N - 1)$
6		poimirlem2.5	$⊢ φ \to M \in ((0 \dots N) ∖ \{V\})$
7		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})$
8	7	simprbi	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun U^{-1}$
9	4 8	syl	$⊢ φ \to Fun U^{-1}$
10		imadif	$⊢ Fun U^{-1} \to U [(1 \dots N) ∖ \{V + 1\}] = U [(1 \dots N)] ∖ U [\{V + 1\}]$
11	9 10	syl	$⊢ φ \to U [(1 \dots N) ∖ \{V + 1\}] = U [(1 \dots N)] ∖ U [\{V + 1\}]$
12		fzp1elp1	$⊢ V \in (1 \dots N - 1) \to V + 1 \in (1 \dots N - 1 + 1)$
13	5 12	syl	$⊢ φ \to V + 1 \in (1 \dots N - 1 + 1)$
14	1	nncnd	$⊢ φ \to N \in ℂ$
15		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
16	14 15	syl	$⊢ φ \to N - 1 + 1 = N$
17	16	oveq2d	$⊢ φ \to (1 \dots N - 1 + 1) = (1 \dots N)$
18	13 17	eleqtrd	$⊢ φ \to V + 1 \in (1 \dots N)$
19		fzsplit	$⊢ V + 1 \in (1 \dots N) \to (1 \dots N) = (1 \dots V + 1) \cup (V + 1 + 1 \dots N)$
20	18 19	syl	$⊢ φ \to (1 \dots N) = (1 \dots V + 1) \cup (V + 1 + 1 \dots N)$
21	20	difeq1d	$⊢ φ \to (1 \dots N) ∖ \{V + 1\} = ((1 \dots V + 1) \cup (V + 1 + 1 \dots N)) ∖ \{V + 1\}$
22		difundir	$⊢ ((1 \dots V + 1) \cup (V + 1 + 1 \dots N)) ∖ \{V + 1\} = ((1 \dots V + 1) ∖ \{V + 1\}) \cup ((V + 1 + 1 \dots N) ∖ \{V + 1\})$
23		elfzuz	$⊢ V \in (1 \dots N - 1) \to V \in ℤ_{\geq 1}$
24	5 23	syl	$⊢ φ \to V \in ℤ_{\geq 1}$
25		fzsuc	$⊢ V \in ℤ_{\geq 1} \to (1 \dots V + 1) = (1 \dots V) \cup \{V + 1\}$
26	24 25	syl	$⊢ φ \to (1 \dots V + 1) = (1 \dots V) \cup \{V + 1\}$
27	26	difeq1d	$⊢ φ \to (1 \dots V + 1) ∖ \{V + 1\} = ((1 \dots V) \cup \{V + 1\}) ∖ \{V + 1\}$
28		difun2	$⊢ ((1 \dots V) \cup \{V + 1\}) ∖ \{V + 1\} = (1 \dots V) ∖ \{V + 1\}$
29		elfzelz	$⊢ V \in (1 \dots N - 1) \to V \in ℤ$
30	5 29	syl	$⊢ φ \to V \in ℤ$
31	30	zred	$⊢ φ \to V \in ℝ$
32	31	ltp1d	$⊢ φ \to V < V + 1$
33	30	peano2zd	$⊢ φ \to V + 1 \in ℤ$
34	33	zred	$⊢ φ \to V + 1 \in ℝ$
35	31 34	ltnled	$⊢ φ \to (V < V + 1 \leftrightarrow \neg V + 1 \leq V)$
36	32 35	mpbid	$⊢ φ \to \neg V + 1 \leq V$
37		elfzle2	$⊢ V + 1 \in (1 \dots V) \to V + 1 \leq V$
38	36 37	nsyl	$⊢ φ \to \neg V + 1 \in (1 \dots V)$
39		difsn	$⊢ \neg V + 1 \in (1 \dots V) \to (1 \dots V) ∖ \{V + 1\} = (1 \dots V)$
40	38 39	syl	$⊢ φ \to (1 \dots V) ∖ \{V + 1\} = (1 \dots V)$
41	28 40	syl5eq	$⊢ φ \to ((1 \dots V) \cup \{V + 1\}) ∖ \{V + 1\} = (1 \dots V)$
42	27 41	eqtrd	$⊢ φ \to (1 \dots V + 1) ∖ \{V + 1\} = (1 \dots V)$
43	34	ltp1d	$⊢ φ \to V + 1 < V + 1 + 1$
44		peano2re	$⊢ V + 1 \in ℝ \to V + 1 + 1 \in ℝ$
45	34 44	syl	$⊢ φ \to V + 1 + 1 \in ℝ$
46	34 45	ltnled	$⊢ φ \to (V + 1 < V + 1 + 1 \leftrightarrow \neg V + 1 + 1 \leq V + 1)$
47	43 46	mpbid	$⊢ φ \to \neg V + 1 + 1 \leq V + 1$
48		elfzle1	$⊢ V + 1 \in (V + 1 + 1 \dots N) \to V + 1 + 1 \leq V + 1$
49	47 48	nsyl	$⊢ φ \to \neg V + 1 \in (V + 1 + 1 \dots N)$
50		difsn	$⊢ \neg V + 1 \in (V + 1 + 1 \dots N) \to (V + 1 + 1 \dots N) ∖ \{V + 1\} = (V + 1 + 1 \dots N)$
51	49 50	syl	$⊢ φ \to (V + 1 + 1 \dots N) ∖ \{V + 1\} = (V + 1 + 1 \dots N)$
52	42 51	uneq12d	$⊢ φ \to ((1 \dots V + 1) ∖ \{V + 1\}) \cup ((V + 1 + 1 \dots N) ∖ \{V + 1\}) = (1 \dots V) \cup (V + 1 + 1 \dots N)$
53	22 52	syl5eq	$⊢ φ \to ((1 \dots V + 1) \cup (V + 1 + 1 \dots N)) ∖ \{V + 1\} = (1 \dots V) \cup (V + 1 + 1 \dots N)$
54	21 53	eqtrd	$⊢ φ \to (1 \dots N) ∖ \{V + 1\} = (1 \dots V) \cup (V + 1 + 1 \dots N)$
55	54	imaeq2d	$⊢ φ \to U [(1 \dots N) ∖ \{V + 1\}] = U [(1 \dots V) \cup (V + 1 + 1 \dots N)]$
56	11 55	eqtr3d	$⊢ φ \to U [(1 \dots N)] ∖ U [\{V + 1\}] = U [(1 \dots V) \cup (V + 1 + 1 \dots N)]$
57		imaundi	$⊢ U [(1 \dots V) \cup (V + 1 + 1 \dots N)] = U [(1 \dots V)] \cup U [(V + 1 + 1 \dots N)]$
58	56 57	eqtrdi	$⊢ φ \to U [(1 \dots N)] ∖ U [\{V + 1\}] = U [(1 \dots V)] \cup U [(V + 1 + 1 \dots N)]$
59	58	eleq2d	$⊢ φ \to (n \in (U [(1 \dots N)] ∖ U [\{V + 1\}]) \leftrightarrow n \in (U [(1 \dots V)] \cup U [(V + 1 + 1 \dots N)]))$
60		eldif	$⊢ n \in (U [(1 \dots N)] ∖ U [\{V + 1\}]) \leftrightarrow (n \in U [(1 \dots N)] \land \neg n \in U [\{V + 1\}])$
61		elun	$⊢ n \in (U [(1 \dots V)] \cup U [(V + 1 + 1 \dots N)]) \leftrightarrow (n \in U [(1 \dots V)] \lor n \in U [(V + 1 + 1 \dots N)])$
62	59 60 61	3bitr3g	$⊢ φ \to ((n \in U [(1 \dots N)] \land \neg n \in U [\{V + 1\}]) \leftrightarrow (n \in U [(1 \dots V)] \lor n \in U [(V + 1 + 1 \dots N)]))$
63	62	adantr	$⊢ (φ \land M < V) \to ((n \in U [(1 \dots N)] \land \neg n \in U [\{V + 1\}]) \leftrightarrow (n \in U [(1 \dots V)] \lor n \in U [(V + 1 + 1 \dots N)]))$
64		imassrn	$⊢ U [(1 \dots V)] \subseteq ran U$
65		f1of	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to U : (1 \dots N) ⟶ (1 \dots N)$
66	4 65	syl	$⊢ φ \to U : (1 \dots N) ⟶ (1 \dots N)$
67	66	frnd	$⊢ φ \to ran U \subseteq (1 \dots N)$
68	64 67	sstrid	$⊢ φ \to U [(1 \dots V)] \subseteq (1 \dots N)$
69	68	sselda	$⊢ (φ \land n \in U [(1 \dots V)]) \to n \in (1 \dots N)$
70	3	ffnd	$⊢ φ \to T Fn (1 \dots N)$
71	70	adantr	$⊢ (φ \land n \in U [(1 \dots V)]) \to T Fn (1 \dots N)$
72		1ex	$⊢ 1 \in V$
73		fnconstg	$⊢ 1 \in V \to (U [(1 \dots V)] \times \{1\}) Fn U [(1 \dots V)]$
74	72 73	ax-mp	$⊢ (U [(1 \dots V)] \times \{1\}) Fn U [(1 \dots V)]$
75		c0ex	$⊢ 0 \in V$
76		fnconstg	$⊢ 0 \in V \to (U [(V + 1 \dots N)] \times \{0\}) Fn U [(V + 1 \dots N)]$
77	75 76	ax-mp	$⊢ (U [(V + 1 \dots N)] \times \{0\}) Fn U [(V + 1 \dots N)]$
78	74 77	pm3.2i	$⊢ ((U [(1 \dots V)] \times \{1\}) Fn U [(1 \dots V)] \land (U [(V + 1 \dots N)] \times \{0\}) Fn U [(V + 1 \dots N)])$
79		imain	$⊢ Fun U^{-1} \to U [(1 \dots V) \cap (V + 1 \dots N)] = U [(1 \dots V)] \cap U [(V + 1 \dots N)]$
80	9 79	syl	$⊢ φ \to U [(1 \dots V) \cap (V + 1 \dots N)] = U [(1 \dots V)] \cap U [(V + 1 \dots N)]$
81		fzdisj	$⊢ V < V + 1 \to (1 \dots V) \cap (V + 1 \dots N) = \emptyset$
82	32 81	syl	$⊢ φ \to (1 \dots V) \cap (V + 1 \dots N) = \emptyset$
83	82	imaeq2d	$⊢ φ \to U [(1 \dots V) \cap (V + 1 \dots N)] = U [\emptyset]$
84		ima0	$⊢ U [\emptyset] = \emptyset$
85	83 84	eqtrdi	$⊢ φ \to U [(1 \dots V) \cap (V + 1 \dots N)] = \emptyset$
86	80 85	eqtr3d	$⊢ φ \to U [(1 \dots V)] \cap U [(V + 1 \dots N)] = \emptyset$
87		fnun	$⊢ (((U [(1 \dots V)] \times \{1\}) Fn U [(1 \dots V)] \land (U [(V + 1 \dots N)] \times \{0\}) Fn U [(V + 1 \dots N)]) \land U [(1 \dots V)] \cap U [(V + 1 \dots N)] = \emptyset) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) Fn (U [(1 \dots V)] \cup U [(V + 1 \dots N)])$
88	78 86 87	sylancr	$⊢ φ \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) Fn (U [(1 \dots V)] \cup U [(V + 1 \dots N)])$
89		imaundi	$⊢ U [(1 \dots V) \cup (V + 1 \dots N)] = U [(1 \dots V)] \cup U [(V + 1 \dots N)]$
90	1	nnzd	$⊢ φ \to N \in ℤ$
91		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
92	90 91	syl	$⊢ φ \to N - 1 \in ℤ$
93		uzid	$⊢ N - 1 \in ℤ \to N - 1 \in ℤ_{\geq (N - 1)}$
94	92 93	syl	$⊢ φ \to N - 1 \in ℤ_{\geq (N - 1)}$
95		peano2uz	$⊢ N - 1 \in ℤ_{\geq (N - 1)} \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
96	94 95	syl	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
97	16 96	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq (N - 1)}$
98		fzss2	$⊢ N \in ℤ_{\geq (N - 1)} \to (1 \dots N - 1) \subseteq (1 \dots N)$
99	97 98	syl	$⊢ φ \to (1 \dots N - 1) \subseteq (1 \dots N)$
100	99 5	sseldd	$⊢ φ \to V \in (1 \dots N)$
101		fzsplit	$⊢ V \in (1 \dots N) \to (1 \dots N) = (1 \dots V) \cup (V + 1 \dots N)$
102	100 101	syl	$⊢ φ \to (1 \dots N) = (1 \dots V) \cup (V + 1 \dots N)$
103	102	imaeq2d	$⊢ φ \to U [(1 \dots N)] = U [(1 \dots V) \cup (V + 1 \dots N)]$
104		f1ofo	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to U : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
105	4 104	syl	$⊢ φ \to U : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
106		foima	$⊢ U : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to U [(1 \dots N)] = (1 \dots N)$
107	105 106	syl	$⊢ φ \to U [(1 \dots N)] = (1 \dots N)$
108	103 107	eqtr3d	$⊢ φ \to U [(1 \dots V) \cup (V + 1 \dots N)] = (1 \dots N)$
109	89 108	syl5eqr	$⊢ φ \to U [(1 \dots V)] \cup U [(V + 1 \dots N)] = (1 \dots N)$
110	109	fneq2d	$⊢ φ \to (((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) Fn (U [(1 \dots V)] \cup U [(V + 1 \dots N)]) \leftrightarrow ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) Fn (1 \dots N))$
111	88 110	mpbid	$⊢ φ \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
112	111	adantr	$⊢ (φ \land n \in U [(1 \dots V)]) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
113		fzfid	$⊢ (φ \land n \in U [(1 \dots V)]) \to (1 \dots N) \in Fin$
114		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
115		eqidd	$⊢ ((φ \land n \in U [(1 \dots V)]) \land n \in (1 \dots N)) \to T (n) = T (n)$
116		fvun1	$⊢ ((U [(1 \dots V)] \times \{1\}) Fn U [(1 \dots V)] \land (U [(V + 1 \dots N)] \times \{0\}) Fn U [(V + 1 \dots N)] \land (U [(1 \dots V)] \cap U [(V + 1 \dots N)] = \emptyset \land n \in U [(1 \dots V)])) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) (n) = (U [(1 \dots V)] \times \{1\}) (n)$
117	74 77 116	mp3an12	$⊢ (U [(1 \dots V)] \cap U [(V + 1 \dots N)] = \emptyset \land n \in U [(1 \dots V)]) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) (n) = (U [(1 \dots V)] \times \{1\}) (n)$
118	86 117	sylan	$⊢ (φ \land n \in U [(1 \dots V)]) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) (n) = (U [(1 \dots V)] \times \{1\}) (n)$
119	72	fvconst2	$⊢ n \in U [(1 \dots V)] \to (U [(1 \dots V)] \times \{1\}) (n) = 1$
120	119	adantl	$⊢ (φ \land n \in U [(1 \dots V)]) \to (U [(1 \dots V)] \times \{1\}) (n) = 1$
121	118 120	eqtrd	$⊢ (φ \land n \in U [(1 \dots V)]) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) (n) = 1$
122	121	adantr	$⊢ ((φ \land n \in U [(1 \dots V)]) \land n \in (1 \dots N)) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) (n) = 1$
123	71 112 113 113 114 115 122	ofval	$⊢ ((φ \land n \in U [(1 \dots V)]) \land n \in (1 \dots N)) \to (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n) = T (n) + 1$
124		fnconstg	$⊢ 1 \in V \to (U [(1 \dots V + 1)] \times \{1\}) Fn U [(1 \dots V + 1)]$
125	72 124	ax-mp	$⊢ (U [(1 \dots V + 1)] \times \{1\}) Fn U [(1 \dots V + 1)]$
126		fnconstg	$⊢ 0 \in V \to (U [(V + 1 + 1 \dots N)] \times \{0\}) Fn U [(V + 1 + 1 \dots N)]$
127	75 126	ax-mp	$⊢ (U [(V + 1 + 1 \dots N)] \times \{0\}) Fn U [(V + 1 + 1 \dots N)]$
128	125 127	pm3.2i	$⊢ ((U [(1 \dots V + 1)] \times \{1\}) Fn U [(1 \dots V + 1)] \land (U [(V + 1 + 1 \dots N)] \times \{0\}) Fn U [(V + 1 + 1 \dots N)])$
129		imain	$⊢ Fun U^{-1} \to U [(1 \dots V + 1) \cap (V + 1 + 1 \dots N)] = U [(1 \dots V + 1)] \cap U [(V + 1 + 1 \dots N)]$
130	9 129	syl	$⊢ φ \to U [(1 \dots V + 1) \cap (V + 1 + 1 \dots N)] = U [(1 \dots V + 1)] \cap U [(V + 1 + 1 \dots N)]$
131		fzdisj	$⊢ V + 1 < V + 1 + 1 \to (1 \dots V + 1) \cap (V + 1 + 1 \dots N) = \emptyset$
132	43 131	syl	$⊢ φ \to (1 \dots V + 1) \cap (V + 1 + 1 \dots N) = \emptyset$
133	132	imaeq2d	$⊢ φ \to U [(1 \dots V + 1) \cap (V + 1 + 1 \dots N)] = U [\emptyset]$
134	133 84	eqtrdi	$⊢ φ \to U [(1 \dots V + 1) \cap (V + 1 + 1 \dots N)] = \emptyset$
135	130 134	eqtr3d	$⊢ φ \to U [(1 \dots V + 1)] \cap U [(V + 1 + 1 \dots N)] = \emptyset$
136		fnun	$⊢ (((U [(1 \dots V + 1)] \times \{1\}) Fn U [(1 \dots V + 1)] \land (U [(V + 1 + 1 \dots N)] \times \{0\}) Fn U [(V + 1 + 1 \dots N)]) \land U [(1 \dots V + 1)] \cap U [(V + 1 + 1 \dots N)] = \emptyset) \to ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) Fn (U [(1 \dots V + 1)] \cup U [(V + 1 + 1 \dots N)])$
137	128 135 136	sylancr	$⊢ φ \to ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) Fn (U [(1 \dots V + 1)] \cup U [(V + 1 + 1 \dots N)])$
138		imaundi	$⊢ U [(1 \dots V + 1) \cup (V + 1 + 1 \dots N)] = U [(1 \dots V + 1)] \cup U [(V + 1 + 1 \dots N)]$
139	20	imaeq2d	$⊢ φ \to U [(1 \dots N)] = U [(1 \dots V + 1) \cup (V + 1 + 1 \dots N)]$
140	139 107	eqtr3d	$⊢ φ \to U [(1 \dots V + 1) \cup (V + 1 + 1 \dots N)] = (1 \dots N)$
141	138 140	syl5eqr	$⊢ φ \to U [(1 \dots V + 1)] \cup U [(V + 1 + 1 \dots N)] = (1 \dots N)$
142	141	fneq2d	$⊢ φ \to (((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) Fn (U [(1 \dots V + 1)] \cup U [(V + 1 + 1 \dots N)]) \leftrightarrow ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) Fn (1 \dots N))$
143	137 142	mpbid	$⊢ φ \to ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
144	143	adantr	$⊢ (φ \land n \in U [(1 \dots V)]) \to ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
145		uzid	$⊢ V \in ℤ \to V \in ℤ_{\geq V}$
146	30 145	syl	$⊢ φ \to V \in ℤ_{\geq V}$
147		peano2uz	$⊢ V \in ℤ_{\geq V} \to V + 1 \in ℤ_{\geq V}$
148	146 147	syl	$⊢ φ \to V + 1 \in ℤ_{\geq V}$
149		fzss2	$⊢ V + 1 \in ℤ_{\geq V} \to (1 \dots V) \subseteq (1 \dots V + 1)$
150	148 149	syl	$⊢ φ \to (1 \dots V) \subseteq (1 \dots V + 1)$
151		imass2	$⊢ (1 \dots V) \subseteq (1 \dots V + 1) \to U [(1 \dots V)] \subseteq U [(1 \dots V + 1)]$
152	150 151	syl	$⊢ φ \to U [(1 \dots V)] \subseteq U [(1 \dots V + 1)]$
153	152	sselda	$⊢ (φ \land n \in U [(1 \dots V)]) \to n \in U [(1 \dots V + 1)]$
154		fvun1	$⊢ ((U [(1 \dots V + 1)] \times \{1\}) Fn U [(1 \dots V + 1)] \land (U [(V + 1 + 1 \dots N)] \times \{0\}) Fn U [(V + 1 + 1 \dots N)] \land (U [(1 \dots V + 1)] \cap U [(V + 1 + 1 \dots N)] = \emptyset \land n \in U [(1 \dots V + 1)])) \to ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) (n) = (U [(1 \dots V + 1)] \times \{1\}) (n)$
155	125 127 154	mp3an12	$⊢ (U [(1 \dots V + 1)] \cap U [(V + 1 + 1 \dots N)] = \emptyset \land n \in U [(1 \dots V + 1)]) \to ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) (n) = (U [(1 \dots V + 1)] \times \{1\}) (n)$
156	135 155	sylan	$⊢ (φ \land n \in U [(1 \dots V + 1)]) \to ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) (n) = (U [(1 \dots V + 1)] \times \{1\}) (n)$
157	72	fvconst2	$⊢ n \in U [(1 \dots V + 1)] \to (U [(1 \dots V + 1)] \times \{1\}) (n) = 1$
158	157	adantl	$⊢ (φ \land n \in U [(1 \dots V + 1)]) \to (U [(1 \dots V + 1)] \times \{1\}) (n) = 1$
159	156 158	eqtrd	$⊢ (φ \land n \in U [(1 \dots V + 1)]) \to ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) (n) = 1$
160	153 159	syldan	$⊢ (φ \land n \in U [(1 \dots V)]) \to ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) (n) = 1$
161	160	adantr	$⊢ ((φ \land n \in U [(1 \dots V)]) \land n \in (1 \dots N)) \to ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) (n) = 1$
162	71 144 113 113 114 115 161	ofval	$⊢ ((φ \land n \in U [(1 \dots V)]) \land n \in (1 \dots N)) \to (T +_{f} ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\}))) (n) = T (n) + 1$
163	123 162	eqtr4d	$⊢ ((φ \land n \in U [(1 \dots V)]) \land n \in (1 \dots N)) \to (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n) = (T +_{f} ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\}))) (n)$
164	69 163	mpdan	$⊢ (φ \land n \in U [(1 \dots V)]) \to (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n) = (T +_{f} ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\}))) (n)$
165		imassrn	$⊢ U [(V + 1 + 1 \dots N)] \subseteq ran U$
166	165 67	sstrid	$⊢ φ \to U [(V + 1 + 1 \dots N)] \subseteq (1 \dots N)$
167	166	sselda	$⊢ (φ \land n \in U [(V + 1 + 1 \dots N)]) \to n \in (1 \dots N)$
168	70	adantr	$⊢ (φ \land n \in U [(V + 1 + 1 \dots N)]) \to T Fn (1 \dots N)$
169	111	adantr	$⊢ (φ \land n \in U [(V + 1 + 1 \dots N)]) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
170		fzfid	$⊢ (φ \land n \in U [(V + 1 + 1 \dots N)]) \to (1 \dots N) \in Fin$
171		eqidd	$⊢ ((φ \land n \in U [(V + 1 + 1 \dots N)]) \land n \in (1 \dots N)) \to T (n) = T (n)$
172		uzid	$⊢ V + 1 \in ℤ \to V + 1 \in ℤ_{\geq (V + 1)}$
173	33 172	syl	$⊢ φ \to V + 1 \in ℤ_{\geq (V + 1)}$
174		peano2uz	$⊢ V + 1 \in ℤ_{\geq (V + 1)} \to V + 1 + 1 \in ℤ_{\geq (V + 1)}$
175	173 174	syl	$⊢ φ \to V + 1 + 1 \in ℤ_{\geq (V + 1)}$
176		fzss1	$⊢ V + 1 + 1 \in ℤ_{\geq (V + 1)} \to (V + 1 + 1 \dots N) \subseteq (V + 1 \dots N)$
177	175 176	syl	$⊢ φ \to (V + 1 + 1 \dots N) \subseteq (V + 1 \dots N)$
178		imass2	$⊢ (V + 1 + 1 \dots N) \subseteq (V + 1 \dots N) \to U [(V + 1 + 1 \dots N)] \subseteq U [(V + 1 \dots N)]$
179	177 178	syl	$⊢ φ \to U [(V + 1 + 1 \dots N)] \subseteq U [(V + 1 \dots N)]$
180	179	sselda	$⊢ (φ \land n \in U [(V + 1 + 1 \dots N)]) \to n \in U [(V + 1 \dots N)]$
181		fvun2	$⊢ ((U [(1 \dots V)] \times \{1\}) Fn U [(1 \dots V)] \land (U [(V + 1 \dots N)] \times \{0\}) Fn U [(V + 1 \dots N)] \land (U [(1 \dots V)] \cap U [(V + 1 \dots N)] = \emptyset \land n \in U [(V + 1 \dots N)])) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) (n) = (U [(V + 1 \dots N)] \times \{0\}) (n)$
182	74 77 181	mp3an12	$⊢ (U [(1 \dots V)] \cap U [(V + 1 \dots N)] = \emptyset \land n \in U [(V + 1 \dots N)]) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) (n) = (U [(V + 1 \dots N)] \times \{0\}) (n)$
183	86 182	sylan	$⊢ (φ \land n \in U [(V + 1 \dots N)]) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) (n) = (U [(V + 1 \dots N)] \times \{0\}) (n)$
184	75	fvconst2	$⊢ n \in U [(V + 1 \dots N)] \to (U [(V + 1 \dots N)] \times \{0\}) (n) = 0$
185	184	adantl	$⊢ (φ \land n \in U [(V + 1 \dots N)]) \to (U [(V + 1 \dots N)] \times \{0\}) (n) = 0$
186	183 185	eqtrd	$⊢ (φ \land n \in U [(V + 1 \dots N)]) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) (n) = 0$
187	180 186	syldan	$⊢ (φ \land n \in U [(V + 1 + 1 \dots N)]) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) (n) = 0$
188	187	adantr	$⊢ ((φ \land n \in U [(V + 1 + 1 \dots N)]) \land n \in (1 \dots N)) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) (n) = 0$
189	168 169 170 170 114 171 188	ofval	$⊢ ((φ \land n \in U [(V + 1 + 1 \dots N)]) \land n \in (1 \dots N)) \to (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n) = T (n) + 0$
190	143	adantr	$⊢ (φ \land n \in U [(V + 1 + 1 \dots N)]) \to ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
191		fvun2	$⊢ ((U [(1 \dots V + 1)] \times \{1\}) Fn U [(1 \dots V + 1)] \land (U [(V + 1 + 1 \dots N)] \times \{0\}) Fn U [(V + 1 + 1 \dots N)] \land (U [(1 \dots V + 1)] \cap U [(V + 1 + 1 \dots N)] = \emptyset \land n \in U [(V + 1 + 1 \dots N)])) \to ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) (n) = (U [(V + 1 + 1 \dots N)] \times \{0\}) (n)$
192	125 127 191	mp3an12	$⊢ (U [(1 \dots V + 1)] \cap U [(V + 1 + 1 \dots N)] = \emptyset \land n \in U [(V + 1 + 1 \dots N)]) \to ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) (n) = (U [(V + 1 + 1 \dots N)] \times \{0\}) (n)$
193	135 192	sylan	$⊢ (φ \land n \in U [(V + 1 + 1 \dots N)]) \to ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) (n) = (U [(V + 1 + 1 \dots N)] \times \{0\}) (n)$
194	75	fvconst2	$⊢ n \in U [(V + 1 + 1 \dots N)] \to (U [(V + 1 + 1 \dots N)] \times \{0\}) (n) = 0$
195	194	adantl	$⊢ (φ \land n \in U [(V + 1 + 1 \dots N)]) \to (U [(V + 1 + 1 \dots N)] \times \{0\}) (n) = 0$
196	193 195	eqtrd	$⊢ (φ \land n \in U [(V + 1 + 1 \dots N)]) \to ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) (n) = 0$
197	196	adantr	$⊢ ((φ \land n \in U [(V + 1 + 1 \dots N)]) \land n \in (1 \dots N)) \to ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) (n) = 0$
198	168 190 170 170 114 171 197	ofval	$⊢ ((φ \land n \in U [(V + 1 + 1 \dots N)]) \land n \in (1 \dots N)) \to (T +_{f} ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\}))) (n) = T (n) + 0$
199	189 198	eqtr4d	$⊢ ((φ \land n \in U [(V + 1 + 1 \dots N)]) \land n \in (1 \dots N)) \to (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n) = (T +_{f} ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\}))) (n)$
200	167 199	mpdan	$⊢ (φ \land n \in U [(V + 1 + 1 \dots N)]) \to (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n) = (T +_{f} ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\}))) (n)$
201	164 200	jaodan	$⊢ (φ \land (n \in U [(1 \dots V)] \lor n \in U [(V + 1 + 1 \dots N)])) \to (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n) = (T +_{f} ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\}))) (n)$
202	201	adantlr	$⊢ ((φ \land M < V) \land (n \in U [(1 \dots V)] \lor n \in U [(V + 1 + 1 \dots N)])) \to (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n) = (T +_{f} ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\}))) (n)$
203	2	adantr	$⊢ (φ \land M < V) \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\}))))$
204		vex	$⊢ y \in V$
205		ovex	$⊢ y + 1 \in V$
206	204 205	ifex	$⊢ if (y < M, y, y + 1) \in V$
207	206	a1i	$⊢ ((φ \land M < V) \land y = V - 1) \to if (y < M, y, y + 1) \in V$
208		breq1	$⊢ y = V - 1 \to (y < M \leftrightarrow V - 1 < M)$
209	208	adantl	$⊢ (φ \land y = V - 1) \to (y < M \leftrightarrow V - 1 < M)$
210		simpr	$⊢ (φ \land y = V - 1) \to y = V - 1$
211		oveq1	$⊢ y = V - 1 \to y + 1 = V - 1 + 1$
212	30	zcnd	$⊢ φ \to V \in ℂ$
213		npcan1	$⊢ V \in ℂ \to V - 1 + 1 = V$
214	212 213	syl	$⊢ φ \to V - 1 + 1 = V$
215	211 214	sylan9eqr	$⊢ (φ \land y = V - 1) \to y + 1 = V$
216	209 210 215	ifbieq12d	$⊢ (φ \land y = V - 1) \to if (y < M, y, y + 1) = if (V - 1 < M, V - 1, V)$
217	216	adantlr	$⊢ ((φ \land M < V) \land y = V - 1) \to if (y < M, y, y + 1) = if (V - 1 < M, V - 1, V)$
218	6	eldifad	$⊢ φ \to M \in (0 \dots N)$
219		elfzelz	$⊢ M \in (0 \dots N) \to M \in ℤ$
220	218 219	syl	$⊢ φ \to M \in ℤ$
221		zltlem1	$⊢ (M \in ℤ \land V \in ℤ) \to (M < V \leftrightarrow M \leq V - 1)$
222	220 30 221	syl2anc	$⊢ φ \to (M < V \leftrightarrow M \leq V - 1)$
223	220	zred	$⊢ φ \to M \in ℝ$
224		peano2zm	$⊢ V \in ℤ \to V - 1 \in ℤ$
225	30 224	syl	$⊢ φ \to V - 1 \in ℤ$
226	225	zred	$⊢ φ \to V - 1 \in ℝ$
227	223 226	lenltd	$⊢ φ \to (M \leq V - 1 \leftrightarrow \neg V - 1 < M)$
228	222 227	bitrd	$⊢ φ \to (M < V \leftrightarrow \neg V - 1 < M)$
229	228	biimpa	$⊢ (φ \land M < V) \to \neg V - 1 < M$
230	229	iffalsed	$⊢ (φ \land M < V) \to if (V - 1 < M, V - 1, V) = V$
231	230	adantr	$⊢ ((φ \land M < V) \land y = V - 1) \to if (V - 1 < M, V - 1, V) = V$
232	217 231	eqtrd	$⊢ ((φ \land M < V) \land y = V - 1) \to if (y < M, y, y + 1) = V$
233	232	eqeq2d	$⊢ ((φ \land M < V) \land y = V - 1) \to (j = if (y < M, y, y + 1) \leftrightarrow j = V)$
234	233	biimpa	$⊢ (((φ \land M < V) \land y = V - 1) \land j = if (y < M, y, y + 1)) \to j = V$
235		oveq2	$⊢ j = V \to (1 \dots j) = (1 \dots V)$
236	235	imaeq2d	$⊢ j = V \to U [(1 \dots j)] = U [(1 \dots V)]$
237	236	xpeq1d	$⊢ j = V \to U [(1 \dots j)] \times \{1\} = U [(1 \dots V)] \times \{1\}$
238		oveq1	$⊢ j = V \to j + 1 = V + 1$
239	238	oveq1d	$⊢ j = V \to (j + 1 \dots N) = (V + 1 \dots N)$
240	239	imaeq2d	$⊢ j = V \to U [(j + 1 \dots N)] = U [(V + 1 \dots N)]$
241	240	xpeq1d	$⊢ j = V \to U [(j + 1 \dots N)] \times \{0\} = U [(V + 1 \dots N)] \times \{0\}$
242	237 241	uneq12d	$⊢ j = V \to (U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}) = (U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})$
243	242	oveq2d	$⊢ j = V \to T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) = T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))$
244	234 243	syl	$⊢ (((φ \land M < V) \land y = V - 1) \land j = if (y < M, y, y + 1)) \to T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) = T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))$
245	207 244	csbied	$⊢ ((φ \land M < V) \land y = V - 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 V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))$
246		elfzm1b	$⊢ (V \in ℤ \land N \in ℤ) \to (V \in (1 \dots N) \leftrightarrow V - 1 \in (0 \dots N - 1))$
247	30 90 246	syl2anc	$⊢ φ \to (V \in (1 \dots N) \leftrightarrow V - 1 \in (0 \dots N - 1))$
248	100 247	mpbid	$⊢ φ \to V - 1 \in (0 \dots N - 1)$
249	248	adantr	$⊢ (φ \land M < V) \to V - 1 \in (0 \dots N - 1)$
250		ovexd	$⊢ (φ \land M < V) \to T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) \in V$
251	203 245 249 250	fvmptd	$⊢ (φ \land M < V) \to F (V - 1) = T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))$
252	251	fveq1d	$⊢ (φ \land M < V) \to F (V - 1) (n) = (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n)$
253	252	adantr	$⊢ ((φ \land M < V) \land (n \in U [(1 \dots V)] \lor n \in U [(V + 1 + 1 \dots N)])) \to F (V - 1) (n) = (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n)$
254	206	a1i	$⊢ ((φ \land M < V) \land y = V) \to if (y < M, y, y + 1) \in V$
255		breq1	$⊢ y = V \to (y < M \leftrightarrow V < M)$
256		id	$⊢ y = V \to y = V$
257		oveq1	$⊢ y = V \to y + 1 = V + 1$
258	255 256 257	ifbieq12d	$⊢ y = V \to if (y < M, y, y + 1) = if (V < M, V, V + 1)$
259		ltnsym	$⊢ (M \in ℝ \land V \in ℝ) \to (M < V \to \neg V < M)$
260	223 31 259	syl2anc	$⊢ φ \to (M < V \to \neg V < M)$
261	260	imp	$⊢ (φ \land M < V) \to \neg V < M$
262	261	iffalsed	$⊢ (φ \land M < V) \to if (V < M, V, V + 1) = V + 1$
263	258 262	sylan9eqr	$⊢ ((φ \land M < V) \land y = V) \to if (y < M, y, y + 1) = V + 1$
264	263	eqeq2d	$⊢ ((φ \land M < V) \land y = V) \to (j = if (y < M, y, y + 1) \leftrightarrow j = V + 1)$
265	264	biimpa	$⊢ (((φ \land M < V) \land y = V) \land j = if (y < M, y, y + 1)) \to j = V + 1$
266		oveq2	$⊢ j = V + 1 \to (1 \dots j) = (1 \dots V + 1)$
267	266	imaeq2d	$⊢ j = V + 1 \to U [(1 \dots j)] = U [(1 \dots V + 1)]$
268	267	xpeq1d	$⊢ j = V + 1 \to U [(1 \dots j)] \times \{1\} = U [(1 \dots V + 1)] \times \{1\}$
269		oveq1	$⊢ j = V + 1 \to j + 1 = V + 1 + 1$
270	269	oveq1d	$⊢ j = V + 1 \to (j + 1 \dots N) = (V + 1 + 1 \dots N)$
271	270	imaeq2d	$⊢ j = V + 1 \to U [(j + 1 \dots N)] = U [(V + 1 + 1 \dots N)]$
272	271	xpeq1d	$⊢ j = V + 1 \to U [(j + 1 \dots N)] \times \{0\} = U [(V + 1 + 1 \dots N)] \times \{0\}$
273	268 272	uneq12d	$⊢ j = V + 1 \to (U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}) = (U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})$
274	273	oveq2d	$⊢ j = V + 1 \to T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) = T +_{f} ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\}))$
275	265 274	syl	$⊢ (((φ \land M < V) \land y = V) \land j = if (y < M, y, y + 1)) \to T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) = T +_{f} ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\}))$
276	254 275	csbied	$⊢ ((φ \land M < V) \land y = V) \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 V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\}))$
277		fz1ssfz0	$⊢ (1 \dots N - 1) \subseteq (0 \dots N - 1)$
278	277 5	sseldi	$⊢ φ \to V \in (0 \dots N - 1)$
279	278	adantr	$⊢ (φ \land M < V) \to V \in (0 \dots N - 1)$
280		ovexd	$⊢ (φ \land M < V) \to T +_{f} ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\})) \in V$
281	203 276 279 280	fvmptd	$⊢ (φ \land M < V) \to F (V) = T +_{f} ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\}))$
282	281	fveq1d	$⊢ (φ \land M < V) \to F (V) (n) = (T +_{f} ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\}))) (n)$
283	282	adantr	$⊢ ((φ \land M < V) \land (n \in U [(1 \dots V)] \lor n \in U [(V + 1 + 1 \dots N)])) \to F (V) (n) = (T +_{f} ((U [(1 \dots V + 1)] \times \{1\}) \cup (U [(V + 1 + 1 \dots N)] \times \{0\}))) (n)$
284	202 253 283	3eqtr4d	$⊢ ((φ \land M < V) \land (n \in U [(1 \dots V)] \lor n \in U [(V + 1 + 1 \dots N)])) \to F (V - 1) (n) = F (V) (n)$
285	284	ex	$⊢ (φ \land M < V) \to ((n \in U [(1 \dots V)] \lor n \in U [(V + 1 + 1 \dots N)]) \to F (V - 1) (n) = F (V) (n))$
286	63 285	sylbid	$⊢ (φ \land M < V) \to ((n \in U [(1 \dots N)] \land \neg n \in U [\{V + 1\}]) \to F (V - 1) (n) = F (V) (n))$
287	286	expdimp	$⊢ ((φ \land M < V) \land n \in U [(1 \dots N)]) \to (\neg n \in U [\{V + 1\}] \to F (V - 1) (n) = F (V) (n))$
288	287	necon1ad	$⊢ ((φ \land M < V) \land n \in U [(1 \dots N)]) \to (F (V - 1) (n) \neq F (V) (n) \to n \in U [\{V + 1\}])$
289		elimasni	$⊢ n \in U [\{V + 1\}] \to (V + 1) U n$
290		eqcom	$⊢ n = U (V + 1) \leftrightarrow U (V + 1) = n$
291		f1ofn	$⊢ U : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to U Fn (1 \dots N)$
292	4 291	syl	$⊢ φ \to U Fn (1 \dots N)$
293		fnbrfvb	$⊢ (U Fn (1 \dots N) \land V + 1 \in (1 \dots N)) \to (U (V + 1) = n \leftrightarrow (V + 1) U n)$
294	292 18 293	syl2anc	$⊢ φ \to (U (V + 1) = n \leftrightarrow (V + 1) U n)$
295	290 294	syl5bb	$⊢ φ \to (n = U (V + 1) \leftrightarrow (V + 1) U n)$
296	289 295	syl5ibr	$⊢ φ \to (n \in U [\{V + 1\}] \to n = U (V + 1))$
297	296	ad2antrr	$⊢ ((φ \land M < V) \land n \in U [(1 \dots N)]) \to (n \in U [\{V + 1\}] \to n = U (V + 1))$
298	288 297	syld	$⊢ ((φ \land M < V) \land n \in U [(1 \dots N)]) \to (F (V - 1) (n) \neq F (V) (n) \to n = U (V + 1))$
299	298	ralrimiva	$⊢ (φ \land M < V) \to \forall n \in U [(1 \dots N)] (F (V - 1) (n) \neq F (V) (n) \to n = U (V + 1))$
300		fvex	$⊢ U (V + 1) \in V$
301		eqeq2	$⊢ m = U (V + 1) \to (n = m \leftrightarrow n = U (V + 1))$
302	301	imbi2d	$⊢ m = U (V + 1) \to ((F (V - 1) (n) \neq F (V) (n) \to n = m) \leftrightarrow (F (V - 1) (n) \neq F (V) (n) \to n = U (V + 1)))$
303	302	ralbidv	$⊢ m = U (V + 1) \to (\forall n \in U [(1 \dots N)] (F (V - 1) (n) \neq F (V) (n) \to n = m) \leftrightarrow \forall n \in U [(1 \dots N)] (F (V - 1) (n) \neq F (V) (n) \to n = U (V + 1)))$
304	300 303	spcev	$⊢ \forall n \in U [(1 \dots N)] (F (V - 1) (n) \neq F (V) (n) \to n = U (V + 1)) \to \exists m \forall n \in U [(1 \dots N)] (F (V - 1) (n) \neq F (V) (n) \to n = m)$
305	299 304	syl	$⊢ (φ \land M < V) \to \exists m \forall n \in U [(1 \dots N)] (F (V - 1) (n) \neq F (V) (n) \to n = m)$
306		imadif	$⊢ Fun U^{-1} \to U [(1 \dots N) ∖ \{V\}] = U [(1 \dots N)] ∖ U [\{V\}]$
307	9 306	syl	$⊢ φ \to U [(1 \dots N) ∖ \{V\}] = U [(1 \dots N)] ∖ U [\{V\}]$
308	102	difeq1d	$⊢ φ \to (1 \dots N) ∖ \{V\} = ((1 \dots V) \cup (V + 1 \dots N)) ∖ \{V\}$
309		difundir	$⊢ ((1 \dots V) \cup (V + 1 \dots N)) ∖ \{V\} = ((1 \dots V) ∖ \{V\}) \cup ((V + 1 \dots N) ∖ \{V\})$
310	214 24	eqeltrd	$⊢ φ \to V - 1 + 1 \in ℤ_{\geq 1}$
311		uzid	$⊢ V - 1 \in ℤ \to V - 1 \in ℤ_{\geq (V - 1)}$
312	225 311	syl	$⊢ φ \to V - 1 \in ℤ_{\geq (V - 1)}$
313		peano2uz	$⊢ V - 1 \in ℤ_{\geq (V - 1)} \to V - 1 + 1 \in ℤ_{\geq (V - 1)}$
314	312 313	syl	$⊢ φ \to V - 1 + 1 \in ℤ_{\geq (V - 1)}$
315	214 314	eqeltrrd	$⊢ φ \to V \in ℤ_{\geq (V - 1)}$
316		fzsplit2	$⊢ (V - 1 + 1 \in ℤ_{\geq 1} \land V \in ℤ_{\geq (V - 1)}) \to (1 \dots V) = (1 \dots V - 1) \cup (V - 1 + 1 \dots V)$
317	310 315 316	syl2anc	$⊢ φ \to (1 \dots V) = (1 \dots V - 1) \cup (V - 1 + 1 \dots V)$
318	214	oveq1d	$⊢ φ \to (V - 1 + 1 \dots V) = (V \dots V)$
319		fzsn	$⊢ V \in ℤ \to (V \dots V) = \{V\}$
320	30 319	syl	$⊢ φ \to (V \dots V) = \{V\}$
321	318 320	eqtrd	$⊢ φ \to (V - 1 + 1 \dots V) = \{V\}$
322	321	uneq2d	$⊢ φ \to (1 \dots V - 1) \cup (V - 1 + 1 \dots V) = (1 \dots V - 1) \cup \{V\}$
323	317 322	eqtrd	$⊢ φ \to (1 \dots V) = (1 \dots V - 1) \cup \{V\}$
324	323	difeq1d	$⊢ φ \to (1 \dots V) ∖ \{V\} = ((1 \dots V - 1) \cup \{V\}) ∖ \{V\}$
325		difun2	$⊢ ((1 \dots V - 1) \cup \{V\}) ∖ \{V\} = (1 \dots V - 1) ∖ \{V\}$
326	31	ltm1d	$⊢ φ \to V - 1 < V$
327	226 31	ltnled	$⊢ φ \to (V - 1 < V \leftrightarrow \neg V \leq V - 1)$
328	326 327	mpbid	$⊢ φ \to \neg V \leq V - 1$
329		elfzle2	$⊢ V \in (1 \dots V - 1) \to V \leq V - 1$
330	328 329	nsyl	$⊢ φ \to \neg V \in (1 \dots V - 1)$
331		difsn	$⊢ \neg V \in (1 \dots V - 1) \to (1 \dots V - 1) ∖ \{V\} = (1 \dots V - 1)$
332	330 331	syl	$⊢ φ \to (1 \dots V - 1) ∖ \{V\} = (1 \dots V - 1)$
333	325 332	syl5eq	$⊢ φ \to ((1 \dots V - 1) \cup \{V\}) ∖ \{V\} = (1 \dots V - 1)$
334	324 333	eqtrd	$⊢ φ \to (1 \dots V) ∖ \{V\} = (1 \dots V - 1)$
335		elfzle1	$⊢ V \in (V + 1 \dots N) \to V + 1 \leq V$
336	36 335	nsyl	$⊢ φ \to \neg V \in (V + 1 \dots N)$
337		difsn	$⊢ \neg V \in (V + 1 \dots N) \to (V + 1 \dots N) ∖ \{V\} = (V + 1 \dots N)$
338	336 337	syl	$⊢ φ \to (V + 1 \dots N) ∖ \{V\} = (V + 1 \dots N)$
339	334 338	uneq12d	$⊢ φ \to ((1 \dots V) ∖ \{V\}) \cup ((V + 1 \dots N) ∖ \{V\}) = (1 \dots V - 1) \cup (V + 1 \dots N)$
340	309 339	syl5eq	$⊢ φ \to ((1 \dots V) \cup (V + 1 \dots N)) ∖ \{V\} = (1 \dots V - 1) \cup (V + 1 \dots N)$
341	308 340	eqtrd	$⊢ φ \to (1 \dots N) ∖ \{V\} = (1 \dots V - 1) \cup (V + 1 \dots N)$
342	341	imaeq2d	$⊢ φ \to U [(1 \dots N) ∖ \{V\}] = U [(1 \dots V - 1) \cup (V + 1 \dots N)]$
343	307 342	eqtr3d	$⊢ φ \to U [(1 \dots N)] ∖ U [\{V\}] = U [(1 \dots V - 1) \cup (V + 1 \dots N)]$
344		imaundi	$⊢ U [(1 \dots V - 1) \cup (V + 1 \dots N)] = U [(1 \dots V - 1)] \cup U [(V + 1 \dots N)]$
345	343 344	eqtrdi	$⊢ φ \to U [(1 \dots N)] ∖ U [\{V\}] = U [(1 \dots V - 1)] \cup U [(V + 1 \dots N)]$
346	345	eleq2d	$⊢ φ \to (n \in (U [(1 \dots N)] ∖ U [\{V\}]) \leftrightarrow n \in (U [(1 \dots V - 1)] \cup U [(V + 1 \dots N)]))$
347		eldif	$⊢ n \in (U [(1 \dots N)] ∖ U [\{V\}]) \leftrightarrow (n \in U [(1 \dots N)] \land \neg n \in U [\{V\}])$
348		elun	$⊢ n \in (U [(1 \dots V - 1)] \cup U [(V + 1 \dots N)]) \leftrightarrow (n \in U [(1 \dots V - 1)] \lor n \in U [(V + 1 \dots N)])$
349	346 347 348	3bitr3g	$⊢ φ \to ((n \in U [(1 \dots N)] \land \neg n \in U [\{V\}]) \leftrightarrow (n \in U [(1 \dots V - 1)] \lor n \in U [(V + 1 \dots N)]))$
350	349	adantr	$⊢ (φ \land V < M) \to ((n \in U [(1 \dots N)] \land \neg n \in U [\{V\}]) \leftrightarrow (n \in U [(1 \dots V - 1)] \lor n \in U [(V + 1 \dots N)]))$
351		imassrn	$⊢ U [(1 \dots V - 1)] \subseteq ran U$
352	351 67	sstrid	$⊢ φ \to U [(1 \dots V - 1)] \subseteq (1 \dots N)$
353	352	sselda	$⊢ (φ \land n \in U [(1 \dots V - 1)]) \to n \in (1 \dots N)$
354	70	adantr	$⊢ (φ \land n \in U [(1 \dots V - 1)]) \to T Fn (1 \dots N)$
355		fnconstg	$⊢ 1 \in V \to (U [(1 \dots V - 1)] \times \{1\}) Fn U [(1 \dots V - 1)]$
356	72 355	ax-mp	$⊢ (U [(1 \dots V - 1)] \times \{1\}) Fn U [(1 \dots V - 1)]$
357		fnconstg	$⊢ 0 \in V \to (U [(V \dots N)] \times \{0\}) Fn U [(V \dots N)]$
358	75 357	ax-mp	$⊢ (U [(V \dots N)] \times \{0\}) Fn U [(V \dots N)]$
359	356 358	pm3.2i	$⊢ ((U [(1 \dots V - 1)] \times \{1\}) Fn U [(1 \dots V - 1)] \land (U [(V \dots N)] \times \{0\}) Fn U [(V \dots N)])$
360		imain	$⊢ Fun U^{-1} \to U [(1 \dots V - 1) \cap (V \dots N)] = U [(1 \dots V - 1)] \cap U [(V \dots N)]$
361	9 360	syl	$⊢ φ \to U [(1 \dots V - 1) \cap (V \dots N)] = U [(1 \dots V - 1)] \cap U [(V \dots N)]$
362		fzdisj	$⊢ V - 1 < V \to (1 \dots V - 1) \cap (V \dots N) = \emptyset$
363	326 362	syl	$⊢ φ \to (1 \dots V - 1) \cap (V \dots N) = \emptyset$
364	363	imaeq2d	$⊢ φ \to U [(1 \dots V - 1) \cap (V \dots N)] = U [\emptyset]$
365	364 84	eqtrdi	$⊢ φ \to U [(1 \dots V - 1) \cap (V \dots N)] = \emptyset$
366	361 365	eqtr3d	$⊢ φ \to U [(1 \dots V - 1)] \cap U [(V \dots N)] = \emptyset$
367		fnun	$⊢ (((U [(1 \dots V - 1)] \times \{1\}) Fn U [(1 \dots V - 1)] \land (U [(V \dots N)] \times \{0\}) Fn U [(V \dots N)]) \land U [(1 \dots V - 1)] \cap U [(V \dots N)] = \emptyset) \to ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) Fn (U [(1 \dots V - 1)] \cup U [(V \dots N)])$
368	359 366 367	sylancr	$⊢ φ \to ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) Fn (U [(1 \dots V - 1)] \cup U [(V \dots N)])$
369		imaundi	$⊢ U [(1 \dots V - 1) \cup (V \dots N)] = U [(1 \dots V - 1)] \cup U [(V \dots N)]$
370		uzss	$⊢ V \in ℤ_{\geq (V - 1)} \to ℤ_{\geq V} \subseteq ℤ_{\geq (V - 1)}$
371	315 370	syl	$⊢ φ \to ℤ_{\geq V} \subseteq ℤ_{\geq (V - 1)}$
372		elfzuz3	$⊢ V \in (1 \dots N - 1) \to N - 1 \in ℤ_{\geq V}$
373	5 372	syl	$⊢ φ \to N - 1 \in ℤ_{\geq V}$
374	371 373	sseldd	$⊢ φ \to N - 1 \in ℤ_{\geq (V - 1)}$
375		peano2uz	$⊢ N - 1 \in ℤ_{\geq (V - 1)} \to N - 1 + 1 \in ℤ_{\geq (V - 1)}$
376	374 375	syl	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq (V - 1)}$
377	16 376	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq (V - 1)}$
378		fzsplit2	$⊢ (V - 1 + 1 \in ℤ_{\geq 1} \land N \in ℤ_{\geq (V - 1)}) \to (1 \dots N) = (1 \dots V - 1) \cup (V - 1 + 1 \dots N)$
379	310 377 378	syl2anc	$⊢ φ \to (1 \dots N) = (1 \dots V - 1) \cup (V - 1 + 1 \dots N)$
380	214	oveq1d	$⊢ φ \to (V - 1 + 1 \dots N) = (V \dots N)$
381	380	uneq2d	$⊢ φ \to (1 \dots V - 1) \cup (V - 1 + 1 \dots N) = (1 \dots V - 1) \cup (V \dots N)$
382	379 381	eqtrd	$⊢ φ \to (1 \dots N) = (1 \dots V - 1) \cup (V \dots N)$
383	382	imaeq2d	$⊢ φ \to U [(1 \dots N)] = U [(1 \dots V - 1) \cup (V \dots N)]$
384	383 107	eqtr3d	$⊢ φ \to U [(1 \dots V - 1) \cup (V \dots N)] = (1 \dots N)$
385	369 384	syl5eqr	$⊢ φ \to U [(1 \dots V - 1)] \cup U [(V \dots N)] = (1 \dots N)$
386	385	fneq2d	$⊢ φ \to (((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) Fn (U [(1 \dots V - 1)] \cup U [(V \dots N)]) \leftrightarrow ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) Fn (1 \dots N))$
387	368 386	mpbid	$⊢ φ \to ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) Fn (1 \dots N)$
388	387	adantr	$⊢ (φ \land n \in U [(1 \dots V - 1)]) \to ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) Fn (1 \dots N)$
389		fzfid	$⊢ (φ \land n \in U [(1 \dots V - 1)]) \to (1 \dots N) \in Fin$
390		eqidd	$⊢ ((φ \land n \in U [(1 \dots V - 1)]) \land n \in (1 \dots N)) \to T (n) = T (n)$
391		fvun1	$⊢ ((U [(1 \dots V - 1)] \times \{1\}) Fn U [(1 \dots V - 1)] \land (U [(V \dots N)] \times \{0\}) Fn U [(V \dots N)] \land (U [(1 \dots V - 1)] \cap U [(V \dots N)] = \emptyset \land n \in U [(1 \dots V - 1)])) \to ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) (n) = (U [(1 \dots V - 1)] \times \{1\}) (n)$
392	356 358 391	mp3an12	$⊢ (U [(1 \dots V - 1)] \cap U [(V \dots N)] = \emptyset \land n \in U [(1 \dots V - 1)]) \to ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) (n) = (U [(1 \dots V - 1)] \times \{1\}) (n)$
393	366 392	sylan	$⊢ (φ \land n \in U [(1 \dots V - 1)]) \to ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) (n) = (U [(1 \dots V - 1)] \times \{1\}) (n)$
394	72	fvconst2	$⊢ n \in U [(1 \dots V - 1)] \to (U [(1 \dots V - 1)] \times \{1\}) (n) = 1$
395	394	adantl	$⊢ (φ \land n \in U [(1 \dots V - 1)]) \to (U [(1 \dots V - 1)] \times \{1\}) (n) = 1$
396	393 395	eqtrd	$⊢ (φ \land n \in U [(1 \dots V - 1)]) \to ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) (n) = 1$
397	396	adantr	$⊢ ((φ \land n \in U [(1 \dots V - 1)]) \land n \in (1 \dots N)) \to ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) (n) = 1$
398	354 388 389 389 114 390 397	ofval	$⊢ ((φ \land n \in U [(1 \dots V - 1)]) \land n \in (1 \dots N)) \to (T +_{f} ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\}))) (n) = T (n) + 1$
399	111	adantr	$⊢ (φ \land n \in U [(1 \dots V - 1)]) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
400		fzss2	$⊢ V \in ℤ_{\geq (V - 1)} \to (1 \dots V - 1) \subseteq (1 \dots V)$
401	315 400	syl	$⊢ φ \to (1 \dots V - 1) \subseteq (1 \dots V)$
402		imass2	$⊢ (1 \dots V - 1) \subseteq (1 \dots V) \to U [(1 \dots V - 1)] \subseteq U [(1 \dots V)]$
403	401 402	syl	$⊢ φ \to U [(1 \dots V - 1)] \subseteq U [(1 \dots V)]$
404	403	sselda	$⊢ (φ \land n \in U [(1 \dots V - 1)]) \to n \in U [(1 \dots V)]$
405	404 121	syldan	$⊢ (φ \land n \in U [(1 \dots V - 1)]) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) (n) = 1$
406	405	adantr	$⊢ ((φ \land n \in U [(1 \dots V - 1)]) \land n \in (1 \dots N)) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) (n) = 1$
407	354 399 389 389 114 390 406	ofval	$⊢ ((φ \land n \in U [(1 \dots V - 1)]) \land n \in (1 \dots N)) \to (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n) = T (n) + 1$
408	398 407	eqtr4d	$⊢ ((φ \land n \in U [(1 \dots V - 1)]) \land n \in (1 \dots N)) \to (T +_{f} ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\}))) (n) = (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n)$
409	353 408	mpdan	$⊢ (φ \land n \in U [(1 \dots V - 1)]) \to (T +_{f} ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\}))) (n) = (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n)$
410		imassrn	$⊢ U [(V + 1 \dots N)] \subseteq ran U$
411	410 67	sstrid	$⊢ φ \to U [(V + 1 \dots N)] \subseteq (1 \dots N)$
412	411	sselda	$⊢ (φ \land n \in U [(V + 1 \dots N)]) \to n \in (1 \dots N)$
413	70	adantr	$⊢ (φ \land n \in U [(V + 1 \dots N)]) \to T Fn (1 \dots N)$
414	387	adantr	$⊢ (φ \land n \in U [(V + 1 \dots N)]) \to ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) Fn (1 \dots N)$
415		fzfid	$⊢ (φ \land n \in U [(V + 1 \dots N)]) \to (1 \dots N) \in Fin$
416		eqidd	$⊢ ((φ \land n \in U [(V + 1 \dots N)]) \land n \in (1 \dots N)) \to T (n) = T (n)$
417		fzss1	$⊢ V + 1 \in ℤ_{\geq V} \to (V + 1 \dots N) \subseteq (V \dots N)$
418	148 417	syl	$⊢ φ \to (V + 1 \dots N) \subseteq (V \dots N)$
419		imass2	$⊢ (V + 1 \dots N) \subseteq (V \dots N) \to U [(V + 1 \dots N)] \subseteq U [(V \dots N)]$
420	418 419	syl	$⊢ φ \to U [(V + 1 \dots N)] \subseteq U [(V \dots N)]$
421	420	sselda	$⊢ (φ \land n \in U [(V + 1 \dots N)]) \to n \in U [(V \dots N)]$
422		fvun2	$⊢ ((U [(1 \dots V - 1)] \times \{1\}) Fn U [(1 \dots V - 1)] \land (U [(V \dots N)] \times \{0\}) Fn U [(V \dots N)] \land (U [(1 \dots V - 1)] \cap U [(V \dots N)] = \emptyset \land n \in U [(V \dots N)])) \to ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) (n) = (U [(V \dots N)] \times \{0\}) (n)$
423	356 358 422	mp3an12	$⊢ (U [(1 \dots V - 1)] \cap U [(V \dots N)] = \emptyset \land n \in U [(V \dots N)]) \to ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) (n) = (U [(V \dots N)] \times \{0\}) (n)$
424	366 423	sylan	$⊢ (φ \land n \in U [(V \dots N)]) \to ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) (n) = (U [(V \dots N)] \times \{0\}) (n)$
425	75	fvconst2	$⊢ n \in U [(V \dots N)] \to (U [(V \dots N)] \times \{0\}) (n) = 0$
426	425	adantl	$⊢ (φ \land n \in U [(V \dots N)]) \to (U [(V \dots N)] \times \{0\}) (n) = 0$
427	424 426	eqtrd	$⊢ (φ \land n \in U [(V \dots N)]) \to ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) (n) = 0$
428	421 427	syldan	$⊢ (φ \land n \in U [(V + 1 \dots N)]) \to ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) (n) = 0$
429	428	adantr	$⊢ ((φ \land n \in U [(V + 1 \dots N)]) \land n \in (1 \dots N)) \to ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) (n) = 0$
430	413 414 415 415 114 416 429	ofval	$⊢ ((φ \land n \in U [(V + 1 \dots N)]) \land n \in (1 \dots N)) \to (T +_{f} ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\}))) (n) = T (n) + 0$
431	111	adantr	$⊢ (φ \land n \in U [(V + 1 \dots N)]) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
432	186	adantr	$⊢ ((φ \land n \in U [(V + 1 \dots N)]) \land n \in (1 \dots N)) \to ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) (n) = 0$
433	413 431 415 415 114 416 432	ofval	$⊢ ((φ \land n \in U [(V + 1 \dots N)]) \land n \in (1 \dots N)) \to (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n) = T (n) + 0$
434	430 433	eqtr4d	$⊢ ((φ \land n \in U [(V + 1 \dots N)]) \land n \in (1 \dots N)) \to (T +_{f} ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\}))) (n) = (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n)$
435	412 434	mpdan	$⊢ (φ \land n \in U [(V + 1 \dots N)]) \to (T +_{f} ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\}))) (n) = (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n)$
436	409 435	jaodan	$⊢ (φ \land (n \in U [(1 \dots V - 1)] \lor n \in U [(V + 1 \dots N)])) \to (T +_{f} ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\}))) (n) = (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n)$
437	436	adantlr	$⊢ ((φ \land V < M) \land (n \in U [(1 \dots V - 1)] \lor n \in U [(V + 1 \dots N)])) \to (T +_{f} ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\}))) (n) = (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n)$
438	2	adantr	$⊢ (φ \land V < M) \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\}))))$
439	206	a1i	$⊢ ((φ \land V < M) \land y = V - 1) \to if (y < M, y, y + 1) \in V$
440	216	adantlr	$⊢ ((φ \land V < M) \land y = V - 1) \to if (y < M, y, y + 1) = if (V - 1 < M, V - 1, V)$
441		lttr	$⊢ (V - 1 \in ℝ \land V \in ℝ \land M \in ℝ) \to ((V - 1 < V \land V < M) \to V - 1 < M)$
442	226 31 223 441	syl3anc	$⊢ φ \to ((V - 1 < V \land V < M) \to V - 1 < M)$
443	326 442	mpand	$⊢ φ \to (V < M \to V - 1 < M)$
444	443	imp	$⊢ (φ \land V < M) \to V - 1 < M$
445	444	iftrued	$⊢ (φ \land V < M) \to if (V - 1 < M, V - 1, V) = V - 1$
446	445	adantr	$⊢ ((φ \land V < M) \land y = V - 1) \to if (V - 1 < M, V - 1, V) = V - 1$
447	440 446	eqtrd	$⊢ ((φ \land V < M) \land y = V - 1) \to if (y < M, y, y + 1) = V - 1$
448		simpll	$⊢ ((φ \land V < M) \land y = V - 1) \to φ$
449		oveq2	$⊢ j = V - 1 \to (1 \dots j) = (1 \dots V - 1)$
450	449	imaeq2d	$⊢ j = V - 1 \to U [(1 \dots j)] = U [(1 \dots V - 1)]$
451	450	xpeq1d	$⊢ j = V - 1 \to U [(1 \dots j)] \times \{1\} = U [(1 \dots V - 1)] \times \{1\}$
452	451	adantl	$⊢ (φ \land j = V - 1) \to U [(1 \dots j)] \times \{1\} = U [(1 \dots V - 1)] \times \{1\}$
453		oveq1	$⊢ j = V - 1 \to j + 1 = V - 1 + 1$
454	453 214	sylan9eqr	$⊢ (φ \land j = V - 1) \to j + 1 = V$
455	454	oveq1d	$⊢ (φ \land j = V - 1) \to (j + 1 \dots N) = (V \dots N)$
456	455	imaeq2d	$⊢ (φ \land j = V - 1) \to U [(j + 1 \dots N)] = U [(V \dots N)]$
457	456	xpeq1d	$⊢ (φ \land j = V - 1) \to U [(j + 1 \dots N)] \times \{0\} = U [(V \dots N)] \times \{0\}$
458	452 457	uneq12d	$⊢ (φ \land j = V - 1) \to (U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\}) = (U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})$
459	458	oveq2d	$⊢ (φ \land j = V - 1) \to T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) = T +_{f} ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\}))$
460	448 459	sylan	$⊢ (((φ \land V < M) \land y = V - 1) \land j = V - 1) \to T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) = T +_{f} ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\}))$
461	439 447 460	csbied2	$⊢ ((φ \land V < M) \land y = V - 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 V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\}))$
462	248	adantr	$⊢ (φ \land V < M) \to V - 1 \in (0 \dots N - 1)$
463		ovexd	$⊢ (φ \land V < M) \to T +_{f} ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\})) \in V$
464	438 461 462 463	fvmptd	$⊢ (φ \land V < M) \to F (V - 1) = T +_{f} ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\}))$
465	464	fveq1d	$⊢ (φ \land V < M) \to F (V - 1) (n) = (T +_{f} ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\}))) (n)$
466	465	adantr	$⊢ ((φ \land V < M) \land (n \in U [(1 \dots V - 1)] \lor n \in U [(V + 1 \dots N)])) \to F (V - 1) (n) = (T +_{f} ((U [(1 \dots V - 1)] \times \{1\}) \cup (U [(V \dots N)] \times \{0\}))) (n)$
467	206	a1i	$⊢ (V < M \land y = V) \to if (y < M, y, y + 1) \in V$
468		iftrue	$⊢ V < M \to if (V < M, V, V + 1) = V$
469	258 468	sylan9eqr	$⊢ (V < M \land y = V) \to if (y < M, y, y + 1) = V$
470	469	eqeq2d	$⊢ (V < M \land y = V) \to (j = if (y < M, y, y + 1) \leftrightarrow j = V)$
471	470	biimpa	$⊢ ((V < M \land y = V) \land j = if (y < M, y, y + 1)) \to j = V$
472	471 243	syl	$⊢ ((V < M \land y = V) \land j = if (y < M, y, y + 1)) \to T +_{f} ((U [(1 \dots j)] \times \{1\}) \cup (U [(j + 1 \dots N)] \times \{0\})) = T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))$
473	467 472	csbied	$⊢ (V < M \land y = V) \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 V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))$
474	473	adantll	$⊢ ((φ \land V < M) \land y = V) \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 V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))$
475	278	adantr	$⊢ (φ \land V < M) \to V \in (0 \dots N - 1)$
476		ovexd	$⊢ (φ \land V < M) \to T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\})) \in V$
477	438 474 475 476	fvmptd	$⊢ (φ \land V < M) \to F (V) = T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))$
478	477	fveq1d	$⊢ (φ \land V < M) \to F (V) (n) = (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n)$
479	478	adantr	$⊢ ((φ \land V < M) \land (n \in U [(1 \dots V - 1)] \lor n \in U [(V + 1 \dots N)])) \to F (V) (n) = (T +_{f} ((U [(1 \dots V)] \times \{1\}) \cup (U [(V + 1 \dots N)] \times \{0\}))) (n)$
480	437 466 479	3eqtr4d	$⊢ ((φ \land V < M) \land (n \in U [(1 \dots V - 1)] \lor n \in U [(V + 1 \dots N)])) \to F (V - 1) (n) = F (V) (n)$
481	480	ex	$⊢ (φ \land V < M) \to ((n \in U [(1 \dots V - 1)] \lor n \in U [(V + 1 \dots N)]) \to F (V - 1) (n) = F (V) (n))$
482	350 481	sylbid	$⊢ (φ \land V < M) \to ((n \in U [(1 \dots N)] \land \neg n \in U [\{V\}]) \to F (V - 1) (n) = F (V) (n))$
483	482	expdimp	$⊢ ((φ \land V < M) \land n \in U [(1 \dots N)]) \to (\neg n \in U [\{V\}] \to F (V - 1) (n) = F (V) (n))$
484	483	necon1ad	$⊢ ((φ \land V < M) \land n \in U [(1 \dots N)]) \to (F (V - 1) (n) \neq F (V) (n) \to n \in U [\{V\}])$
485		elimasni	$⊢ n \in U [\{V\}] \to V U n$
486		eqcom	$⊢ n = U (V) \leftrightarrow U (V) = n$
487		fnbrfvb	$⊢ (U Fn (1 \dots N) \land V \in (1 \dots N)) \to (U (V) = n \leftrightarrow V U n)$
488	292 100 487	syl2anc	$⊢ φ \to (U (V) = n \leftrightarrow V U n)$
489	486 488	syl5bb	$⊢ φ \to (n = U (V) \leftrightarrow V U n)$
490	485 489	syl5ibr	$⊢ φ \to (n \in U [\{V\}] \to n = U (V))$
491	490	ad2antrr	$⊢ ((φ \land V < M) \land n \in U [(1 \dots N)]) \to (n \in U [\{V\}] \to n = U (V))$
492	484 491	syld	$⊢ ((φ \land V < M) \land n \in U [(1 \dots N)]) \to (F (V - 1) (n) \neq F (V) (n) \to n = U (V))$
493	492	ralrimiva	$⊢ (φ \land V < M) \to \forall n \in U [(1 \dots N)] (F (V - 1) (n) \neq F (V) (n) \to n = U (V))$
494		fvex	$⊢ U (V) \in V$
495		eqeq2	$⊢ m = U (V) \to (n = m \leftrightarrow n = U (V))$
496	495	imbi2d	$⊢ m = U (V) \to ((F (V - 1) (n) \neq F (V) (n) \to n = m) \leftrightarrow (F (V - 1) (n) \neq F (V) (n) \to n = U (V)))$
497	496	ralbidv	$⊢ m = U (V) \to (\forall n \in U [(1 \dots N)] (F (V - 1) (n) \neq F (V) (n) \to n = m) \leftrightarrow \forall n \in U [(1 \dots N)] (F (V - 1) (n) \neq F (V) (n) \to n = U (V)))$
498	494 497	spcev	$⊢ \forall n \in U [(1 \dots N)] (F (V - 1) (n) \neq F (V) (n) \to n = U (V)) \to \exists m \forall n \in U [(1 \dots N)] (F (V - 1) (n) \neq F (V) (n) \to n = m)$
499	493 498	syl	$⊢ (φ \land V < M) \to \exists m \forall n \in U [(1 \dots N)] (F (V - 1) (n) \neq F (V) (n) \to n = m)$
500		eldifsni	$⊢ M \in ((0 \dots N) ∖ \{V\}) \to M \neq V$
501	6 500	syl	$⊢ φ \to M \neq V$
502	223 31	lttri2d	$⊢ φ \to (M \neq V \leftrightarrow (M < V \lor V < M))$
503	501 502	mpbid	$⊢ φ \to (M < V \lor V < M)$
504	305 499 503	mpjaodan	$⊢ φ \to \exists m \forall n \in U [(1 \dots N)] (F (V - 1) (n) \neq F (V) (n) \to n = m)$
505		nfv	$⊢ Ⅎ m F (V - 1) (n) \neq F (V) (n)$
506	505	rmo2	$⊢ \exists^{*} n \in U [(1 \dots N)] F (V - 1) (n) \neq F (V) (n) \leftrightarrow \exists m \forall n \in U [(1 \dots N)] (F (V - 1) (n) \neq F (V) (n) \to n = m)$
507		rmoeq1	$⊢ U [(1 \dots N)] = (1 \dots N) \to (\exists^{} n \in U [(1 \dots N)] F (V - 1) (n) \neq F (V) (n) \leftrightarrow \exists^{} n \in (1 \dots N) F (V - 1) (n) \neq F (V) (n))$
508	107 507	syl	$⊢ φ \to (\exists^{} n \in U [(1 \dots N)] F (V - 1) (n) \neq F (V) (n) \leftrightarrow \exists^{} n \in (1 \dots N) F (V - 1) (n) \neq F (V) (n))$
509	506 508	bitr3id	$⊢ φ \to (\exists m \forall n \in U [(1 \dots N)] (F (V - 1) (n) \neq F (V) (n) \to n = m) \leftrightarrow \exists^{*} n \in (1 \dots N) F (V - 1) (n) \neq F (V) (n))$
510	504 509	mpbid	$⊢ φ \to \exists^{*} n \in (1 \dots N) F (V - 1) (n) \neq F (V) (n)$

Metamath Proof Explorer

Theorem poimirlem2

Proof