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

Metamath Proof Explorer

Theorem poimirlem2

Proof