poimirlem6

Description: Lemma for poimir establishing, for a face of a simplex defined by a walk along the edges of an N -cube, the single dimension in which successive vertices before the opposite vertex differ. (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	poimir.0	$⊢ φ \to N \in ℕ$
	poimirlem22.s	$⊢ S = \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\}$
	poimirlem9.1	$⊢ φ \to T \in S$
	poimirlem9.2	$⊢ φ \to 2^{nd} (T) \in (1 \dots N - 1)$
	poimirlem6.3	$⊢ φ \to M \in (1 \dots 2^{nd} (T) - 1)$
Assertion	poimirlem6	$⊢ φ \to (ι n \in (1 \dots N) \| F (M - 1) (n) \neq F (M) (n)) = 2^{nd} (1^{st} (T)) (M)$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$⊢ φ \to N \in ℕ$
2		poimirlem22.s	$⊢ S = \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\}$
3		poimirlem9.1	$⊢ φ \to T \in S$
4		poimirlem9.2	$⊢ φ \to 2^{nd} (T) \in (1 \dots N - 1)$
5		poimirlem6.3	$⊢ φ \to M \in (1 \dots 2^{nd} (T) - 1)$
6		elrabi	$⊢ T \in \{t \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \| F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))))\} \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
7	6 2	eleq2s	$⊢ T \in S \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
8	3 7	syl	$⊢ φ \to T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N))$
9		xp1st	$⊢ T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
10	8 9	syl	$⊢ φ \to 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
11		xp2nd	$⊢ 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
12	10 11	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
13		fvex	$⊢ 2^{nd} (1^{st} (T)) \in V$
14		f1oeq1	$⊢ f = 2^{nd} (1^{st} (T)) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
15	13 14	elab	$⊢ 2^{nd} (1^{st} (T)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
16	12 15	sylib	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
17		f1of	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) : (1 \dots N) ⟶ (1 \dots N)$
18	16 17	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) ⟶ (1 \dots N)$
19		elfznn	$⊢ 2^{nd} (T) \in (1 \dots N - 1) \to 2^{nd} (T) \in ℕ$
20	4 19	syl	$⊢ φ \to 2^{nd} (T) \in ℕ$
21	20	nnzd	$⊢ φ \to 2^{nd} (T) \in ℤ$
22		peano2zm	$⊢ 2^{nd} (T) \in ℤ \to 2^{nd} (T) - 1 \in ℤ$
23	21 22	syl	$⊢ φ \to 2^{nd} (T) - 1 \in ℤ$
24	1	nnzd	$⊢ φ \to N \in ℤ$
25	23	zred	$⊢ φ \to 2^{nd} (T) - 1 \in ℝ$
26	20	nnred	$⊢ φ \to 2^{nd} (T) \in ℝ$
27	1	nnred	$⊢ φ \to N \in ℝ$
28	26	lem1d	$⊢ φ \to 2^{nd} (T) - 1 \leq 2^{nd} (T)$
29		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
30	1 29	syl	$⊢ φ \to N - 1 \in ℕ_{0}$
31	30	nn0red	$⊢ φ \to N - 1 \in ℝ$
32		elfzle2	$⊢ 2^{nd} (T) \in (1 \dots N - 1) \to 2^{nd} (T) \leq N - 1$
33	4 32	syl	$⊢ φ \to 2^{nd} (T) \leq N - 1$
34	27	lem1d	$⊢ φ \to N - 1 \leq N$
35	26 31 27 33 34	letrd	$⊢ φ \to 2^{nd} (T) \leq N$
36	25 26 27 28 35	letrd	$⊢ φ \to 2^{nd} (T) - 1 \leq N$
37		eluz2	$⊢ N \in ℤ_{\geq (2^{nd} (T) - 1)} \leftrightarrow (2^{nd} (T) - 1 \in ℤ \land N \in ℤ \land 2^{nd} (T) - 1 \leq N)$
38	23 24 36 37	syl3anbrc	$⊢ φ \to N \in ℤ_{\geq (2^{nd} (T) - 1)}$
39		fzss2	$⊢ N \in ℤ_{\geq (2^{nd} (T) - 1)} \to (1 \dots 2^{nd} (T) - 1) \subseteq (1 \dots N)$
40	38 39	syl	$⊢ φ \to (1 \dots 2^{nd} (T) - 1) \subseteq (1 \dots N)$
41	40 5	sseldd	$⊢ φ \to M \in (1 \dots N)$
42	18 41	ffvelrnd	$⊢ φ \to 2^{nd} (1^{st} (T)) (M) \in (1 \dots N)$
43		xp1st	$⊢ 1^{st} (T) \in (({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
44	10 43	syl	$⊢ φ \to 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)})$
45		elmapfn	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
46	44 45	syl	$⊢ φ \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
47	46	adantr	$⊢ (φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \to 1^{st} (1^{st} (T)) Fn (1 \dots N)$
48		1ex	$⊢ 1 \in V$
49		fnconstg	$⊢ 1 \in V \to (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M - 1)]$
50	48 49	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M - 1)]$
51		c0ex	$⊢ 0 \in V$
52		fnconstg	$⊢ 0 \in V \to (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M \dots N)]$
53	51 52	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M \dots N)]$
54	50 53	pm3.2i	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \land (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M \dots N)])$
55		dff1o3	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow (2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \land Fun {2^{nd} (1^{st} (T))}^{-1})$
56	55	simprbi	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun {2^{nd} (1^{st} (T))}^{-1}$
57	16 56	syl	$⊢ φ \to Fun {2^{nd} (1^{st} (T))}^{-1}$
58		imain	$⊢ Fun {2^{nd} (1^{st} (T))}^{-1} \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cap (M \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M \dots N)]$
59	57 58	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cap (M \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M \dots N)]$
60		elfznn	$⊢ M \in (1 \dots 2^{nd} (T) - 1) \to M \in ℕ$
61	5 60	syl	$⊢ φ \to M \in ℕ$
62	61	nnred	$⊢ φ \to M \in ℝ$
63	62	ltm1d	$⊢ φ \to M - 1 < M$
64		fzdisj	$⊢ M - 1 < M \to (1 \dots M - 1) \cap (M \dots N) = \emptyset$
65	63 64	syl	$⊢ φ \to (1 \dots M - 1) \cap (M \dots N) = \emptyset$
66	65	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cap (M \dots N)] = 2^{nd} (1^{st} (T)) [\emptyset]$
67		ima0	$⊢ 2^{nd} (1^{st} (T)) [\emptyset] = \emptyset$
68	66 67	syl6eq	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cap (M \dots N)] = \emptyset$
69	59 68	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M \dots N)] = \emptyset$
70		fnun	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \land (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M \dots N)]) \land 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M \dots N)] = \emptyset) \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M \dots N)])$
71	54 69 70	sylancr	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M \dots N)])$
72	61	nncnd	$⊢ φ \to M \in ℂ$
73		npcan1	$⊢ M \in ℂ \to M - 1 + 1 = M$
74	72 73	syl	$⊢ φ \to M - 1 + 1 = M$
75		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
76	61 75	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 1}$
77	74 76	eqeltrd	$⊢ φ \to M - 1 + 1 \in ℤ_{\geq 1}$
78		nnm1nn0	$⊢ M \in ℕ \to M - 1 \in ℕ_{0}$
79	61 78	syl	$⊢ φ \to M - 1 \in ℕ_{0}$
80	79	nn0zd	$⊢ φ \to M - 1 \in ℤ$
81		uzid	$⊢ M - 1 \in ℤ \to M - 1 \in ℤ_{\geq (M - 1)}$
82	80 81	syl	$⊢ φ \to M - 1 \in ℤ_{\geq (M - 1)}$
83		peano2uz	$⊢ M - 1 \in ℤ_{\geq (M - 1)} \to M - 1 + 1 \in ℤ_{\geq (M - 1)}$
84	82 83	syl	$⊢ φ \to M - 1 + 1 \in ℤ_{\geq (M - 1)}$
85	74 84	eqeltrrd	$⊢ φ \to M \in ℤ_{\geq (M - 1)}$
86		uzss	$⊢ M \in ℤ_{\geq (M - 1)} \to ℤ_{\geq M} \subseteq ℤ_{\geq (M - 1)}$
87	85 86	syl	$⊢ φ \to ℤ_{\geq M} \subseteq ℤ_{\geq (M - 1)}$
88	61	nnzd	$⊢ φ \to M \in ℤ$
89		elfzle2	$⊢ M \in (1 \dots 2^{nd} (T) - 1) \to M \leq 2^{nd} (T) - 1$
90	5 89	syl	$⊢ φ \to M \leq 2^{nd} (T) - 1$
91	62 25 27 90 36	letrd	$⊢ φ \to M \leq N$
92		eluz2	$⊢ N \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land N \in ℤ \land M \leq N)$
93	88 24 91 92	syl3anbrc	$⊢ φ \to N \in ℤ_{\geq M}$
94	87 93	sseldd	$⊢ φ \to N \in ℤ_{\geq (M - 1)}$
95		fzsplit2	$⊢ (M - 1 + 1 \in ℤ_{\geq 1} \land N \in ℤ_{\geq (M - 1)}) \to (1 \dots N) = (1 \dots M - 1) \cup (M - 1 + 1 \dots N)$
96	77 94 95	syl2anc	$⊢ φ \to (1 \dots N) = (1 \dots M - 1) \cup (M - 1 + 1 \dots N)$
97	74	oveq1d	$⊢ φ \to (M - 1 + 1 \dots N) = (M \dots N)$
98	97	uneq2d	$⊢ φ \to (1 \dots M - 1) \cup (M - 1 + 1 \dots N) = (1 \dots M - 1) \cup (M \dots N)$
99	96 98	eqtrd	$⊢ φ \to (1 \dots N) = (1 \dots M - 1) \cup (M \dots N)$
100	99	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cup (M \dots N)]$
101		imaundi	$⊢ 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cup (M \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M \dots N)]$
102	100 101	syl6eq	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M \dots N)]$
103		f1ofo	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
104	16 103	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
105		foima	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = (1 \dots N)$
106	104 105	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = (1 \dots N)$
107	102 106	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M \dots N)] = (1 \dots N)$
108	107	fneq2d	$⊢ φ \to (((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M \dots N)]) \leftrightarrow ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) Fn (1 \dots N))$
109	71 108	mpbid	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) Fn (1 \dots N)$
110	109	adantr	$⊢ (φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) Fn (1 \dots N)$
111		ovexd	$⊢ (φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \to (1 \dots N) \in V$
112		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
113		eqidd	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (n) = 1^{st} (1^{st} (T)) (n)$
114		imaundi	$⊢ 2^{nd} (1^{st} (T)) [\{M\} \cup (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [\{M\}] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
115		fzpred	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = \{M\} \cup (M + 1 \dots N)$
116	93 115	syl	$⊢ φ \to (M \dots N) = \{M\} \cup (M + 1 \dots N)$
117	116	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(M \dots N)] = 2^{nd} (1^{st} (T)) [\{M\} \cup (M + 1 \dots N)]$
118		f1ofn	$⊢ 2^{nd} (1^{st} (T)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (1^{st} (T)) Fn (1 \dots N)$
119	16 118	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) Fn (1 \dots N)$
120		fnsnfv	$⊢ (2^{nd} (1^{st} (T)) Fn (1 \dots N) \land M \in (1 \dots N)) \to \{2^{nd} (1^{st} (T)) (M)\} = 2^{nd} (1^{st} (T)) [\{M\}]$
121	119 41 120	syl2anc	$⊢ φ \to \{2^{nd} (1^{st} (T)) (M)\} = 2^{nd} (1^{st} (T)) [\{M\}]$
122	121	uneq1d	$⊢ φ \to \{2^{nd} (1^{st} (T)) (M)\} \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [\{M\}] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
123	114 117 122	3eqtr4a	$⊢ φ \to 2^{nd} (1^{st} (T)) [(M \dots N)] = \{2^{nd} (1^{st} (T)) (M)\} \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
124	123	xpeq1d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\} = (\{2^{nd} (1^{st} (T)) (M)\} \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]) \times \{0\}$
125		xpundir	$⊢ (\{2^{nd} (1^{st} (T)) (M)\} \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]) \times \{0\} = (\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})$
126	124 125	syl6eq	$⊢ φ \to 2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\} = (\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})$
127	126	uneq2d	$⊢ φ \to (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
128		un12	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) = (\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
129	127 128	syl6eq	$⊢ φ \to (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) = (\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
130	129	fveq1d	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) (n) = ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
131	130	ad2antrr	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) (n) = ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
132		fnconstg	$⊢ 0 \in V \to (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
133	51 132	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
134	50 133	pm3.2i	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \land (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)])$
135		imain	$⊢ Fun {2^{nd} (1^{st} (T))}^{-1} \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
136	57 135	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
137	79	nn0red	$⊢ φ \to M - 1 \in ℝ$
138		peano2re	$⊢ M \in ℝ \to M + 1 \in ℝ$
139	62 138	syl	$⊢ φ \to M + 1 \in ℝ$
140	62	ltp1d	$⊢ φ \to M < M + 1$
141	137 62 139 63 140	lttrd	$⊢ φ \to M - 1 < M + 1$
142		fzdisj	$⊢ M - 1 < M + 1 \to (1 \dots M - 1) \cap (M + 1 \dots N) = \emptyset$
143	141 142	syl	$⊢ φ \to (1 \dots M - 1) \cap (M + 1 \dots N) = \emptyset$
144	143	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [\emptyset]$
145	144 67	syl6eq	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cap (M + 1 \dots N)] = \emptyset$
146	136 145	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset$
147		fnun	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \land (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]) \land 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset) \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)])$
148	134 146 147	sylancr	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)])$
149		imaundi	$⊢ 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cup (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
150		imadif	$⊢ Fun {2^{nd} (1^{st} (T))}^{-1} \to 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{M\}] = 2^{nd} (1^{st} (T)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (T)) [\{M\}]$
151	57 150	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{M\}] = 2^{nd} (1^{st} (T)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (T)) [\{M\}]$
152		fzsplit	$⊢ M \in (1 \dots N) \to (1 \dots N) = (1 \dots M) \cup (M + 1 \dots N)$
153	41 152	syl	$⊢ φ \to (1 \dots N) = (1 \dots M) \cup (M + 1 \dots N)$
154	153	difeq1d	$⊢ φ \to (1 \dots N) ∖ \{M\} = ((1 \dots M) \cup (M + 1 \dots N)) ∖ \{M\}$
155		difundir	$⊢ ((1 \dots M) \cup (M + 1 \dots N)) ∖ \{M\} = ((1 \dots M) ∖ \{M\}) \cup ((M + 1 \dots N) ∖ \{M\})$
156		fzsplit2	$⊢ (M - 1 + 1 \in ℤ_{\geq 1} \land M \in ℤ_{\geq (M - 1)}) \to (1 \dots M) = (1 \dots M - 1) \cup (M - 1 + 1 \dots M)$
157	77 85 156	syl2anc	$⊢ φ \to (1 \dots M) = (1 \dots M - 1) \cup (M - 1 + 1 \dots M)$
158	74	oveq1d	$⊢ φ \to (M - 1 + 1 \dots M) = (M \dots M)$
159		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
160	88 159	syl	$⊢ φ \to (M \dots M) = \{M\}$
161	158 160	eqtrd	$⊢ φ \to (M - 1 + 1 \dots M) = \{M\}$
162	161	uneq2d	$⊢ φ \to (1 \dots M - 1) \cup (M - 1 + 1 \dots M) = (1 \dots M - 1) \cup \{M\}$
163	157 162	eqtrd	$⊢ φ \to (1 \dots M) = (1 \dots M - 1) \cup \{M\}$
164	163	difeq1d	$⊢ φ \to (1 \dots M) ∖ \{M\} = ((1 \dots M - 1) \cup \{M\}) ∖ \{M\}$
165		difun2	$⊢ ((1 \dots M - 1) \cup \{M\}) ∖ \{M\} = (1 \dots M - 1) ∖ \{M\}$
166	137 62	ltnled	$⊢ φ \to (M - 1 < M \leftrightarrow \neg M \leq M - 1)$
167	63 166	mpbid	$⊢ φ \to \neg M \leq M - 1$
168		elfzle2	$⊢ M \in (1 \dots M - 1) \to M \leq M - 1$
169	167 168	nsyl	$⊢ φ \to \neg M \in (1 \dots M - 1)$
170		difsn	$⊢ \neg M \in (1 \dots M - 1) \to (1 \dots M - 1) ∖ \{M\} = (1 \dots M - 1)$
171	169 170	syl	$⊢ φ \to (1 \dots M - 1) ∖ \{M\} = (1 \dots M - 1)$
172	165 171	syl5eq	$⊢ φ \to ((1 \dots M - 1) \cup \{M\}) ∖ \{M\} = (1 \dots M - 1)$
173	164 172	eqtrd	$⊢ φ \to (1 \dots M) ∖ \{M\} = (1 \dots M - 1)$
174	62 139	ltnled	$⊢ φ \to (M < M + 1 \leftrightarrow \neg M + 1 \leq M)$
175	140 174	mpbid	$⊢ φ \to \neg M + 1 \leq M$
176		elfzle1	$⊢ M \in (M + 1 \dots N) \to M + 1 \leq M$
177	175 176	nsyl	$⊢ φ \to \neg M \in (M + 1 \dots N)$
178		difsn	$⊢ \neg M \in (M + 1 \dots N) \to (M + 1 \dots N) ∖ \{M\} = (M + 1 \dots N)$
179	177 178	syl	$⊢ φ \to (M + 1 \dots N) ∖ \{M\} = (M + 1 \dots N)$
180	173 179	uneq12d	$⊢ φ \to ((1 \dots M) ∖ \{M\}) \cup ((M + 1 \dots N) ∖ \{M\}) = (1 \dots M - 1) \cup (M + 1 \dots N)$
181	155 180	syl5eq	$⊢ φ \to ((1 \dots M) \cup (M + 1 \dots N)) ∖ \{M\} = (1 \dots M - 1) \cup (M + 1 \dots N)$
182	154 181	eqtrd	$⊢ φ \to (1 \dots N) ∖ \{M\} = (1 \dots M - 1) \cup (M + 1 \dots N)$
183	182	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N) ∖ \{M\}] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cup (M + 1 \dots N)]$
184	121	eqcomd	$⊢ φ \to 2^{nd} (1^{st} (T)) [\{M\}] = \{2^{nd} (1^{st} (T)) (M)\}$
185	106 184	difeq12d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] ∖ 2^{nd} (1^{st} (T)) [\{M\}] = (1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}$
186	151 183 185	3eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cup (M + 1 \dots N)] = (1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}$
187	149 186	syl5eqr	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = (1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}$
188	187	fneq2d	$⊢ φ \to (((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]) \leftrightarrow ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}))$
189	148 188	mpbid	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\})$
190		eldifsn	$⊢ n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) \leftrightarrow (n \in (1 \dots N) \land n \neq 2^{nd} (1^{st} (T)) (M))$
191	190	biimpri	$⊢ (n \in (1 \dots N) \land n \neq 2^{nd} (1^{st} (T)) (M)) \to n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\})$
192	191	ancoms	$⊢ (n \neq 2^{nd} (1^{st} (T)) (M) \land n \in (1 \dots N)) \to n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\})$
193		disjdif	$⊢ \{2^{nd} (1^{st} (T)) (M)\} \cap ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) = \emptyset$
194		fnconstg	$⊢ 0 \in V \to (\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) Fn \{2^{nd} (1^{st} (T)) (M)\}$
195	51 194	ax-mp	$⊢ (\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) Fn \{2^{nd} (1^{st} (T)) (M)\}$
196		fvun2	$⊢ ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) Fn \{2^{nd} (1^{st} (T)) (M)\} \land ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) \land (\{2^{nd} (1^{st} (T)) (M)\} \cap ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) = \emptyset \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}))) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
197	195 196	mp3an1	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) \land (\{2^{nd} (1^{st} (T)) (M)\} \cap ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) = \emptyset \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}))) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
198	193 197	mpanr1	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\})) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
199	189 192 198	syl2an	$⊢ (φ \land (n \neq 2^{nd} (1^{st} (T)) (M) \land n \in (1 \dots N))) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
200	199	anassrs	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{0\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
201	131 200	eqtrd	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
202	47 110 111 111 112 113 201	ofval	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (n) = 1^{st} (1^{st} (T)) (n) + ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
203		fnconstg	$⊢ 1 \in V \to (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)]$
204	48 203	ax-mp	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)]$
205	204 133	pm3.2i	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)] \land (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)])$
206		imain	$⊢ Fun {2^{nd} (1^{st} (T))}^{-1} \to 2^{nd} (1^{st} (T)) [(1 \dots M) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
207	57 206	syl	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
208		fzdisj	$⊢ M < M + 1 \to (1 \dots M) \cap (M + 1 \dots N) = \emptyset$
209	140 208	syl	$⊢ φ \to (1 \dots M) \cap (M + 1 \dots N) = \emptyset$
210	209	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M) \cap (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [\emptyset]$
211	210 67	syl6eq	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M) \cap (M + 1 \dots N)] = \emptyset$
212	207 211	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset$
213		fnun	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)] \land (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]) \land 2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)])$
214	205 212 213	sylancr	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)])$
215	153	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M) \cup (M + 1 \dots N)]$
216		imaundi	$⊢ 2^{nd} (1^{st} (T)) [(1 \dots M) \cup (M + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
217	215 216	syl6eq	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots N)] = 2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
218	217 106	eqtr3d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = (1 \dots N)$
219	218	fneq2d	$⊢ φ \to (((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (2^{nd} (1^{st} (T)) [(1 \dots M)] \cup 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]) \leftrightarrow ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (1 \dots N))$
220	214 219	mpbid	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
221	220	adantr	$⊢ (φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
222		imaundi	$⊢ 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cup \{M\}] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [\{M\}]$
223	163	imaeq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1) \cup \{M\}]$
224	121	uneq2d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup \{2^{nd} (1^{st} (T)) (M)\} = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup 2^{nd} (1^{st} (T)) [\{M\}]$
225	222 223 224	3eqtr4a	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup \{2^{nd} (1^{st} (T)) (M)\}$
226	225	xpeq1d	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\} = (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup \{2^{nd} (1^{st} (T)) (M)\}) \times \{1\}$
227		xpundir	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cup \{2^{nd} (1^{st} (T)) (M)\}) \times \{1\} = (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\})$
228	226 227	syl6eq	$⊢ φ \to 2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\} = (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\})$
229	228	uneq1d	$⊢ φ \to (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\})) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})$
230		un23	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\})) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) \cup (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\})$
231	230	equncomi	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\})) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) = (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
232	229 231	syl6eq	$⊢ φ \to (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) = (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
233	232	fveq1d	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n) = ((\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
234	233	ad2antrr	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n) = ((\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
235		fnconstg	$⊢ 1 \in V \to (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) Fn \{2^{nd} (1^{st} (T)) (M)\}$
236	48 235	ax-mp	$⊢ (\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) Fn \{2^{nd} (1^{st} (T)) (M)\}$
237		fvun2	$⊢ ((\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) Fn \{2^{nd} (1^{st} (T)) (M)\} \land ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) \land (\{2^{nd} (1^{st} (T)) (M)\} \cap ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) = \emptyset \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}))) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
238	236 237	mp3an1	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) \land (\{2^{nd} (1^{st} (T)) (M)\} \cap ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) = \emptyset \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}))) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
239	193 238	mpanr1	$⊢ (((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) Fn ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\}) \land n \in ((1 \dots N) ∖ \{2^{nd} (1^{st} (T)) (M)\})) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
240	189 192 239	syl2an	$⊢ (φ \land (n \neq 2^{nd} (1^{st} (T)) (M) \land n \in (1 \dots N))) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
241	240	anassrs	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to ((\{2^{nd} (1^{st} (T)) (M)\} \times \{1\}) \cup ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
242	234 241	eqtrd	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n) = ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
243	47 221 111 111 112 113 242	ofval	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n) = 1^{st} (1^{st} (T)) (n) + ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (n)$
244	202 243	eqtr4d	$⊢ ((φ \land n \neq 2^{nd} (1^{st} (T)) (M)) \land n \in (1 \dots N)) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (n) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
245	244	an32s	$⊢ ((φ \land n \in (1 \dots N)) \land n \neq 2^{nd} (1^{st} (T)) (M)) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (n) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
246	245	anasss	$⊢ (φ \land (n \in (1 \dots N) \land n \neq 2^{nd} (1^{st} (T)) (M))) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (n) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
247		fveq2	$⊢ t = T \to 2^{nd} (t) = 2^{nd} (T)$
248	247	breq2d	$⊢ t = T \to (y < 2^{nd} (t) \leftrightarrow y < 2^{nd} (T))$
249	248	ifbid	$⊢ t = T \to if (y < 2^{nd} (t), y, y + 1) = if (y < 2^{nd} (T), y, y + 1)$
250	249	csbeq1d	$⊢ t = T \to ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))$
251		2fveq3	$⊢ t = T \to 1^{st} (1^{st} (t)) = 1^{st} (1^{st} (T))$
252		2fveq3	$⊢ t = T \to 2^{nd} (1^{st} (t)) = 2^{nd} (1^{st} (T))$
253	252	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots j)]$
254	253	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}$
255	252	imaeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)]$
256	255	xpeq1d	$⊢ t = T \to 2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}$
257	254 256	uneq12d	$⊢ t = T \to (2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})$
258	251 257	oveq12d	$⊢ t = T \to 1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))$
259	258	csbeq2dv	$⊢ t = T \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
260	250 259	eqtrd	$⊢ t = T \to ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
261	260	mpteq2dv	$⊢ t = T \to (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))) = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
262	261	eqeq2d	$⊢ t = T \to (F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (t), y, y + 1) / j ⦌ (1^{st} (1^{st} (t)) +_{f} ((2^{nd} (1^{st} (t)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (t)) [(j + 1 \dots N)] \times \{0\})))) \leftrightarrow F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))))$
263	262 2	elrab2	$⊢ T \in S \leftrightarrow (T \in ((({(0 ..^K)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \times (0 \dots N)) \land F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))))$
264	263	simprbi	$⊢ T \in S \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
265	3 264	syl	$⊢ φ \to F = (y \in (0 \dots N - 1) ⟼ ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))))$
266		breq1	$⊢ y = M - 1 \to (y < 2^{nd} (T) \leftrightarrow M - 1 < 2^{nd} (T))$
267		id	$⊢ y = M - 1 \to y = M - 1$
268	266 267	ifbieq1d	$⊢ y = M - 1 \to if (y < 2^{nd} (T), y, y + 1) = if (M - 1 < 2^{nd} (T), M - 1, y + 1)$
269	26	ltm1d	$⊢ φ \to 2^{nd} (T) - 1 < 2^{nd} (T)$
270	62 25 26 90 269	lelttrd	$⊢ φ \to M < 2^{nd} (T)$
271	137 62 26 63 270	lttrd	$⊢ φ \to M - 1 < 2^{nd} (T)$
272	271	iftrued	$⊢ φ \to if (M - 1 < 2^{nd} (T), M - 1, y + 1) = M - 1$
273	268 272	sylan9eqr	$⊢ (φ \land y = M - 1) \to if (y < 2^{nd} (T), y, y + 1) = M - 1$
274	273	csbeq1d	$⊢ (φ \land y = M - 1) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ (M - 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
275		oveq2	$⊢ j = M - 1 \to (1 \dots j) = (1 \dots M - 1)$
276	275	imaeq2d	$⊢ j = M - 1 \to 2^{nd} (1^{st} (T)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)]$
277	276	xpeq1d	$⊢ j = M - 1 \to 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}$
278	277	adantl	$⊢ (φ \land j = M - 1) \to 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}$
279		oveq1	$⊢ j = M - 1 \to j + 1 = M - 1 + 1$
280	279 74	sylan9eqr	$⊢ (φ \land j = M - 1) \to j + 1 = M$
281	280	oveq1d	$⊢ (φ \land j = M - 1) \to (j + 1 \dots N) = (M \dots N)$
282	281	imaeq2d	$⊢ (φ \land j = M - 1) \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(M \dots N)]$
283	282	xpeq1d	$⊢ (φ \land j = M - 1) \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}$
284	278 283	uneq12d	$⊢ (φ \land j = M - 1) \to (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})$
285	284	oveq2d	$⊢ (φ \land j = M - 1) \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))$
286	79 285	csbied	$⊢ φ \to ⦋ (M - 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))$
287	286	adantr	$⊢ (φ \land y = M - 1) \to ⦋ (M - 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))$
288	274 287	eqtrd	$⊢ (φ \land y = M - 1) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))$
289		1red	$⊢ φ \to 1 \in ℝ$
290	62 27 289 91	lesub1dd	$⊢ φ \to M - 1 \leq N - 1$
291		elfz2nn0	$⊢ M - 1 \in (0 \dots N - 1) \leftrightarrow (M - 1 \in ℕ_{0} \land N - 1 \in ℕ_{0} \land M - 1 \leq N - 1)$
292	79 30 290 291	syl3anbrc	$⊢ φ \to M - 1 \in (0 \dots N - 1)$
293		ovexd	$⊢ φ \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) \in V$
294	265 288 292 293	fvmptd	$⊢ φ \to F (M - 1) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))$
295	294	fveq1d	$⊢ φ \to F (M - 1) (n) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (n)$
296	295	adantr	$⊢ (φ \land (n \in (1 \dots N) \land n \neq 2^{nd} (1^{st} (T)) (M))) \to F (M - 1) (n) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (n)$
297		breq1	$⊢ y = M \to (y < 2^{nd} (T) \leftrightarrow M < 2^{nd} (T))$
298		id	$⊢ y = M \to y = M$
299	297 298	ifbieq1d	$⊢ y = M \to if (y < 2^{nd} (T), y, y + 1) = if (M < 2^{nd} (T), M, y + 1)$
300	270	iftrued	$⊢ φ \to if (M < 2^{nd} (T), M, y + 1) = M$
301	299 300	sylan9eqr	$⊢ (φ \land y = M) \to if (y < 2^{nd} (T), y, y + 1) = M$
302	301	csbeq1d	$⊢ (φ \land y = M) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = ⦋ M / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})))$
303		oveq2	$⊢ j = M \to (1 \dots j) = (1 \dots M)$
304	303	imaeq2d	$⊢ j = M \to 2^{nd} (1^{st} (T)) [(1 \dots j)] = 2^{nd} (1^{st} (T)) [(1 \dots M)]$
305	304	xpeq1d	$⊢ j = M \to 2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\} = 2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}$
306		oveq1	$⊢ j = M \to j + 1 = M + 1$
307	306	oveq1d	$⊢ j = M \to (j + 1 \dots N) = (M + 1 \dots N)$
308	307	imaeq2d	$⊢ j = M \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] = 2^{nd} (1^{st} (T)) [(M + 1 \dots N)]$
309	308	xpeq1d	$⊢ j = M \to 2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}$
310	305 309	uneq12d	$⊢ j = M \to (2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})$
311	310	oveq2d	$⊢ j = M \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
312	311	adantl	$⊢ (φ \land j = M) \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
313	5 312	csbied	$⊢ φ \to ⦋ M / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
314	313	adantr	$⊢ (φ \land y = M) \to ⦋ M / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
315	302 314	eqtrd	$⊢ (φ \land y = M) \to ⦋ if (y < 2^{nd} (T), y, y + 1) / j ⦌ (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(j + 1 \dots N)] \times \{0\}))) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
316	30	nn0zd	$⊢ φ \to N - 1 \in ℤ$
317	26 27 289 35	lesub1dd	$⊢ φ \to 2^{nd} (T) - 1 \leq N - 1$
318		eluz2	$⊢ N - 1 \in ℤ_{\geq (2^{nd} (T) - 1)} \leftrightarrow (2^{nd} (T) - 1 \in ℤ \land N - 1 \in ℤ \land 2^{nd} (T) - 1 \leq N - 1)$
319	23 316 317 318	syl3anbrc	$⊢ φ \to N - 1 \in ℤ_{\geq (2^{nd} (T) - 1)}$
320		fzss2	$⊢ N - 1 \in ℤ_{\geq (2^{nd} (T) - 1)} \to (1 \dots 2^{nd} (T) - 1) \subseteq (1 \dots N - 1)$
321	319 320	syl	$⊢ φ \to (1 \dots 2^{nd} (T) - 1) \subseteq (1 \dots N - 1)$
322		fz1ssfz0	$⊢ (1 \dots N - 1) \subseteq (0 \dots N - 1)$
323	321 322	sstrdi	$⊢ φ \to (1 \dots 2^{nd} (T) - 1) \subseteq (0 \dots N - 1)$
324	323 5	sseldd	$⊢ φ \to M \in (0 \dots N - 1)$
325		ovexd	$⊢ φ \to 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) \in V$
326	265 315 324 325	fvmptd	$⊢ φ \to F (M) = 1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))$
327	326	fveq1d	$⊢ φ \to F (M) (n) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
328	327	adantr	$⊢ (φ \land (n \in (1 \dots N) \land n \neq 2^{nd} (1^{st} (T)) (M))) \to F (M) (n) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (n)$
329	246 296 328	3eqtr4d	$⊢ (φ \land (n \in (1 \dots N) \land n \neq 2^{nd} (1^{st} (T)) (M))) \to F (M - 1) (n) = F (M) (n)$
330	329	expr	$⊢ (φ \land n \in (1 \dots N)) \to (n \neq 2^{nd} (1^{st} (T)) (M) \to F (M - 1) (n) = F (M) (n))$
331	330	necon1d	$⊢ (φ \land n \in (1 \dots N)) \to (F (M - 1) (n) \neq F (M) (n) \to n = 2^{nd} (1^{st} (T)) (M))$
332		elmapi	$⊢ 1^{st} (1^{st} (T)) \in ({(0 ..^K)}^{(1 \dots N)}) \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
333	44 332	syl	$⊢ φ \to 1^{st} (1^{st} (T)) : (1 \dots N) ⟶ (0 ..^K)$
334	333 42	ffvelrnd	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) \in (0 ..^K)$
335		elfzonn0	$⊢ 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) \in (0 ..^K) \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) \in ℕ_{0}$
336	334 335	syl	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) \in ℕ_{0}$
337	336	nn0red	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) \in ℝ$
338	337	ltp1d	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) < 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) + 1$
339	337 338	ltned	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) \neq 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) + 1$
340	294	fveq1d	$⊢ φ \to F (M - 1) (2^{nd} (1^{st} (T)) (M)) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (2^{nd} (1^{st} (T)) (M))$
341		ovexd	$⊢ φ \to (1 \dots N) \in V$
342		eqidd	$⊢ (φ \land 2^{nd} (1^{st} (T)) (M) \in (1 \dots N)) \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M))$
343		fzss1	$⊢ M \in ℤ_{\geq 1} \to (M \dots N) \subseteq (1 \dots N)$
344	76 343	syl	$⊢ φ \to (M \dots N) \subseteq (1 \dots N)$
345		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
346	93 345	syl	$⊢ φ \to M \in (M \dots N)$
347		fnfvima	$⊢ (2^{nd} (1^{st} (T)) Fn (1 \dots N) \land (M \dots N) \subseteq (1 \dots N) \land M \in (M \dots N)) \to 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(M \dots N)]$
348	119 344 346 347	syl3anc	$⊢ φ \to 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(M \dots N)]$
349		fvun2	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \land (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M \dots N)] \land (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M \dots N)] = \emptyset \land 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(M \dots N)])) \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (M))$
350	50 53 349	mp3an12	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \cap 2^{nd} (1^{st} (T)) [(M \dots N)] = \emptyset \land 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(M \dots N)]) \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (M))$
351	69 348 350	syl2anc	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (M))$
352	51	fvconst2	$⊢ 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(M \dots N)] \to (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (M)) = 0$
353	348 352	syl	$⊢ φ \to (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}) (2^{nd} (1^{st} (T)) (M)) = 0$
354	351 353	eqtrd	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = 0$
355	354	adantr	$⊢ (φ \land 2^{nd} (1^{st} (T)) (M) \in (1 \dots N)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = 0$
356	46 109 341 341 112 342 355	ofval	$⊢ (φ \land 2^{nd} (1^{st} (T)) (M) \in (1 \dots N)) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (2^{nd} (1^{st} (T)) (M)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) + 0$
357	42 356	mpdan	$⊢ φ \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M - 1)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M \dots N)] \times \{0\}))) (2^{nd} (1^{st} (T)) (M)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) + 0$
358	336	nn0cnd	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) \in ℂ$
359	358	addid1d	$⊢ φ \to 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) + 0 = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M))$
360	340 357 359	3eqtrd	$⊢ φ \to F (M - 1) (2^{nd} (1^{st} (T)) (M)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M))$
361	326	fveq1d	$⊢ φ \to F (M) (2^{nd} (1^{st} (T)) (M)) = (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (2^{nd} (1^{st} (T)) (M))$
362		fzss2	$⊢ N \in ℤ_{\geq M} \to (1 \dots M) \subseteq (1 \dots N)$
363	93 362	syl	$⊢ φ \to (1 \dots M) \subseteq (1 \dots N)$
364		elfz1end	$⊢ M \in ℕ \leftrightarrow M \in (1 \dots M)$
365	61 364	sylib	$⊢ φ \to M \in (1 \dots M)$
366		fnfvima	$⊢ (2^{nd} (1^{st} (T)) Fn (1 \dots N) \land (1 \dots M) \subseteq (1 \dots N) \land M \in (1 \dots M)) \to 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(1 \dots M)]$
367	119 363 365 366	syl3anc	$⊢ φ \to 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(1 \dots M)]$
368		fvun1	$⊢ ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) Fn 2^{nd} (1^{st} (T)) [(1 \dots M)] \land (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}) Fn 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \land (2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset \land 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(1 \dots M)])) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) (2^{nd} (1^{st} (T)) (M))$
369	204 133 368	mp3an12	$⊢ (2^{nd} (1^{st} (T)) [(1 \dots M)] \cap 2^{nd} (1^{st} (T)) [(M + 1 \dots N)] = \emptyset \land 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(1 \dots M)]) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) (2^{nd} (1^{st} (T)) (M))$
370	212 367 369	syl2anc	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) (2^{nd} (1^{st} (T)) (M))$
371	48	fvconst2	$⊢ 2^{nd} (1^{st} (T)) (M) \in 2^{nd} (1^{st} (T)) [(1 \dots M)] \to (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) (2^{nd} (1^{st} (T)) (M)) = 1$
372	367 371	syl	$⊢ φ \to (2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) (2^{nd} (1^{st} (T)) (M)) = 1$
373	370 372	eqtrd	$⊢ φ \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = 1$
374	373	adantr	$⊢ (φ \land 2^{nd} (1^{st} (T)) (M) \in (1 \dots N)) \to ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\})) (2^{nd} (1^{st} (T)) (M)) = 1$
375	46 220 341 341 112 342 374	ofval	$⊢ (φ \land 2^{nd} (1^{st} (T)) (M) \in (1 \dots N)) \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (2^{nd} (1^{st} (T)) (M)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) + 1$
376	42 375	mpdan	$⊢ φ \to (1^{st} (1^{st} (T)) +_{f} ((2^{nd} (1^{st} (T)) [(1 \dots M)] \times \{1\}) \cup (2^{nd} (1^{st} (T)) [(M + 1 \dots N)] \times \{0\}))) (2^{nd} (1^{st} (T)) (M)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) + 1$
377	361 376	eqtrd	$⊢ φ \to F (M) (2^{nd} (1^{st} (T)) (M)) = 1^{st} (1^{st} (T)) (2^{nd} (1^{st} (T)) (M)) + 1$
378	339 360 377	3netr4d	$⊢ φ \to F (M - 1) (2^{nd} (1^{st} (T)) (M)) \neq F (M) (2^{nd} (1^{st} (T)) (M))$
379		fveq2	$⊢ n = 2^{nd} (1^{st} (T)) (M) \to F (M - 1) (n) = F (M - 1) (2^{nd} (1^{st} (T)) (M))$
380		fveq2	$⊢ n = 2^{nd} (1^{st} (T)) (M) \to F (M) (n) = F (M) (2^{nd} (1^{st} (T)) (M))$
381	379 380	neeq12d	$⊢ n = 2^{nd} (1^{st} (T)) (M) \to (F (M - 1) (n) \neq F (M) (n) \leftrightarrow F (M - 1) (2^{nd} (1^{st} (T)) (M)) \neq F (M) (2^{nd} (1^{st} (T)) (M)))$
382	378 381	syl5ibrcom	$⊢ φ \to (n = 2^{nd} (1^{st} (T)) (M) \to F (M - 1) (n) \neq F (M) (n))$
383	382	adantr	$⊢ (φ \land n \in (1 \dots N)) \to (n = 2^{nd} (1^{st} (T)) (M) \to F (M - 1) (n) \neq F (M) (n))$
384	331 383	impbid	$⊢ (φ \land n \in (1 \dots N)) \to (F (M - 1) (n) \neq F (M) (n) \leftrightarrow n = 2^{nd} (1^{st} (T)) (M))$
385	42 384	riota5	$⊢ φ \to (ι n \in (1 \dots N) \| F (M - 1) (n) \neq F (M) (n)) = 2^{nd} (1^{st} (T)) (M)$

Metamath Proof Explorer

Theorem poimirlem6

Proof