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

Metamath Proof Explorer

Theorem poimirlem2

Proof