poimirlem7 - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > poimirlem7		Structured version Visualization version GIF version

Theorem poimirlem7 34451

Description: Lemma for poimir 34477, similar to poimirlem6 34450, but for vertices after the opposite vertex. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0	⊢ (𝜑 → 𝑁 ∈ ℕ)
poimirlem22.s	⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
poimirlem9.1	⊢ (𝜑 → 𝑇 ∈ 𝑆)
poimirlem9.2	⊢ (𝜑 → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
poimirlem7.3	⊢ (𝜑 → 𝑀 ∈ ((((2^nd ‘𝑇) + 1) + 1)...𝑁))

**Assertion**
Ref	Expression
poimirlem7	⊢ (𝜑 → (℩𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)) = ((2^nd ‘(1^st ‘𝑇))‘𝑀))

Distinct variable groups: 𝑓,𝑗,𝑛,𝑡,𝑦 𝜑,𝑗,𝑛,𝑦 𝑗,𝐹,𝑛,𝑦 𝑗,𝑀,𝑛,𝑦 𝑗,𝑁,𝑛,𝑦 𝑇,𝑗,𝑛,𝑦 𝜑,𝑡 𝑓,𝐾,𝑗,𝑛,𝑡 𝑓,𝑀,𝑡 𝑓,𝑁,𝑡 𝑇,𝑓 𝑓,𝐹,𝑡 𝑡,𝑇 𝑆,𝑗,𝑛,𝑡,𝑦 Allowed substitution hints: 𝜑(𝑓) 𝑆(𝑓) 𝐾(𝑦)

**Proof of Theorem poimirlem7**
Step	Hyp	Ref	Expression
1		poimirlem9.1	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ 𝑆)
2		elrabi 3616	. . . . . . . . 9 ⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
3		poimirlem22.s	. . . . . . . . 9 ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
4	2, 3	eleq2s 2903	. . . . . . . 8 ⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
5	1, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
6		xp1st 7584	. . . . . . 7 ⊢ (𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
7	5, 6	syl 17	. . . . . 6 ⊢ (𝜑 → (1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
8		xp2nd 7585	. . . . . 6 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
9	7, 8	syl 17	. . . . 5 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
10		fvex 6558	. . . . . 6 ⊢ (2^nd ‘(1^st ‘𝑇)) ∈ V
11		f1oeq1 6479	. . . . . 6 ⊢ (𝑓 = (2^nd ‘(1^st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
12	10, 11	elab 3608	. . . . 5 ⊢ ((2^nd ‘(1^st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
13	9, 12	sylib 219	. . . 4 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
14		f1of 6490	. . . 4 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)⟶(1...𝑁))
15	13, 14	syl 17	. . 3 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)⟶(1...𝑁))
16		poimirlem9.2	. . . . . . . . 9 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ (1...(𝑁 − 1)))
17		elfznn 12790	. . . . . . . . 9 ⊢ ((2^nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^nd ‘𝑇) ∈ ℕ)
18	16, 17	syl 17	. . . . . . . 8 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℕ)
19	18	peano2nnd 11509	. . . . . . 7 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ ℕ)
20	19	peano2nnd 11509	. . . . . 6 ⊢ (𝜑 → (((2^nd ‘𝑇) + 1) + 1) ∈ ℕ)
21		nnuz 12134	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
22	20, 21	syl6eleq 2895	. . . . 5 ⊢ (𝜑 → (((2^nd ‘𝑇) + 1) + 1) ∈ (ℤ_≥‘1))
23		fzss1 12800	. . . . 5 ⊢ ((((2^nd ‘𝑇) + 1) + 1) ∈ (ℤ_≥‘1) → ((((2^nd ‘𝑇) + 1) + 1)...𝑁) ⊆ (1...𝑁))
24	22, 23	syl 17	. . . 4 ⊢ (𝜑 → ((((2^nd ‘𝑇) + 1) + 1)...𝑁) ⊆ (1...𝑁))
25		poimirlem7.3	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ((((2^nd ‘𝑇) + 1) + 1)...𝑁))
26	24, 25	sseldd 3896	. . 3 ⊢ (𝜑 → 𝑀 ∈ (1...𝑁))
27	15, 26	ffvelrnd 6724	. 2 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∈ (1...𝑁))
28		xp1st 7584	. . . . . . . . . . . . 13 ⊢ ((1^st ‘𝑇) ∈ (((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)))
29	7, 28	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)))
30		elmapfn 8286	. . . . . . . . . . . 12 ⊢ ((1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)) → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
31	29, 30	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
32	31	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)) → (1^st ‘(1^st ‘𝑇)) Fn (1...𝑁))
33		1ex 10490	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ V
34		fnconstg 6442	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ V → (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))))
35	33, 34	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1)))
36		c0ex 10488	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
37		fnconstg 6442	. . . . . . . . . . . . . . 15 ⊢ (0 ∈ V → (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)))
38	36, 37	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁))
39	35, 38	pm3.2i 471	. . . . . . . . . . . . 13 ⊢ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∧ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)))
40		dff1o3 6496	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡(2^nd ‘(1^st ‘𝑇))))
41	40	simprbi 497	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡(2^nd ‘(1^st ‘𝑇)))
42	13, 41	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun ^◡(2^nd ‘(1^st ‘𝑇)))
43		imain 6316	. . . . . . . . . . . . . . 15 ⊢ (Fun ^◡(2^nd ‘(1^st ‘𝑇)) → ((2^nd ‘(1^st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁))))
44	42, 43	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁))))
45		elfzelz 12762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ ((((2^nd ‘𝑇) + 1) + 1)...𝑁) → 𝑀 ∈ ℤ)
46	25, 45	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℤ)
47	46	zred 11941	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ ℝ)
48	47	ltm1d 11426	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 − 1) < 𝑀)
49		fzdisj 12788	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 − 1) < 𝑀 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅)
50	48, 49	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅)
51	50	imaeq2d 5813	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((2^nd ‘(1^st ‘𝑇)) “ ∅))
52		ima0 5828	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ∅) = ∅
53	51, 52	syl6eq 2849	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ∅)
54	44, 53	eqtr3d 2835	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁))) = ∅)
55		fnun 6340	. . . . . . . . . . . . 13 ⊢ ((((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∧ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁))) ∧ (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁))) = ∅) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁))))
56	39, 54, 55	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁))))
57	46	zcnd 11942	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℂ)
58		npcan1 10919	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀)
59	57, 58	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
60		1red 10495	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 1 ∈ ℝ)
61	20	nnred 11507	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((2^nd ‘𝑇) + 1) + 1) ∈ ℝ)
62	19	nnred 11507	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ∈ ℝ)
63	19	nnge1d 11539	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ≤ ((2^nd ‘𝑇) + 1))
64	62	ltp1d 11424	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) < (((2^nd ‘𝑇) + 1) + 1))
65	60, 62, 61, 63, 64	lelttrd 10651	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 1 < (((2^nd ‘𝑇) + 1) + 1))
66		elfzle1 12764	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑀 ∈ ((((2^nd ‘𝑇) + 1) + 1)...𝑁) → (((2^nd ‘𝑇) + 1) + 1) ≤ 𝑀)
67	25, 66	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((2^nd ‘𝑇) + 1) + 1) ≤ 𝑀)
68	60, 61, 47, 65, 67	ltletrd 10653	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 1 < 𝑀)
69	60, 47, 68	ltled 10641	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ≤ 𝑀)
70		elnnz1 11862	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℤ ∧ 1 ≤ 𝑀))
71	46, 69, 70	sylanbrc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℕ)
72	71, 21	syl6eleq 2895	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
73	59, 72	eqeltrd 2885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑀 − 1) + 1) ∈ (ℤ_≥‘1))
74		peano2zm 11879	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
75	46, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑀 − 1) ∈ ℤ)
76		uzid 12112	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 − 1) ∈ ℤ → (𝑀 − 1) ∈ (ℤ_≥‘(𝑀 − 1)))
77		peano2uz 12154	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 − 1) ∈ (ℤ_≥‘(𝑀 − 1)) → ((𝑀 − 1) + 1) ∈ (ℤ_≥‘(𝑀 − 1)))
78	75, 76, 77	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑀 − 1) + 1) ∈ (ℤ_≥‘(𝑀 − 1)))
79	59, 78	eqeltrrd 2886	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘(𝑀 − 1)))
80		uzss 12118	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (ℤ_≥‘(𝑀 − 1)) → (ℤ_≥‘𝑀) ⊆ (ℤ_≥‘(𝑀 − 1)))
81	79, 80	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℤ_≥‘𝑀) ⊆ (ℤ_≥‘(𝑀 − 1)))
82		elfzuz3 12759	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ ((((2^nd ‘𝑇) + 1) + 1)...𝑁) → 𝑁 ∈ (ℤ_≥‘𝑀))
83	25, 82	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
84	81, 83	sseldd 3896	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑀 − 1)))
85		fzsplit2 12786	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑀 − 1) + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘(𝑀 − 1))) → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)))
86	73, 84, 85	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)))
87	59	oveq1d 7038	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑁) = (𝑀...𝑁))
88	87	uneq2d 4066	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))
89	86, 88	eqtrd 2833	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))
90	89	imaeq2d 5813	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))))
91		imaundi 5891	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)))
92	90, 91	syl6eq 2849	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁))))
93		f1ofo 6497	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁))
94	13, 93	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁))
95		foima 6470	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (1...𝑁))
96	94, 95	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (1...𝑁))
97	92, 96	eqtr3d 2835	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁))) = (1...𝑁))
98	97	fneq2d 6324	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁))) ↔ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (1...𝑁)))
99	56, 98	mpbid 233	. . . . . . . . . . 11 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))
100	99	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))
101		ovexd 7057	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)) → (1...𝑁) ∈ V)
102		inidm 4121	. . . . . . . . . 10 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
103		eqidd 2798	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘𝑛) = ((1^st ‘(1^st ‘𝑇))‘𝑛))
104		imaundi 5891	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ({𝑀} ∪ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ {𝑀}) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
105		fzpred 12809	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁)))
106	83, 105	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁)))
107	106	imaeq2d 5813	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ({𝑀} ∪ ((𝑀 + 1)...𝑁))))
108		f1ofn 6491	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2^nd ‘(1^st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁))
109	13, 108	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁))
110		fnsnfv 6617	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁) ∧ 𝑀 ∈ (1...𝑁)) → {((2^nd ‘(1^st ‘𝑇))‘𝑀)} = ((2^nd ‘(1^st ‘𝑇)) “ {𝑀}))
111	109, 26, 110	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {((2^nd ‘(1^st ‘𝑇))‘𝑀)} = ((2^nd ‘(1^st ‘𝑇)) “ {𝑀}))
112	111	uneq1d 4065	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ({((2^nd ‘(1^st ‘𝑇))‘𝑀)} ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ {𝑀}) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
113	104, 107, 112	3eqtr4a 2859	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) = ({((2^nd ‘(1^st ‘𝑇))‘𝑀)} ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
114	113	xpeq1d 5479	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}) = (({((2^nd ‘(1^st ‘𝑇))‘𝑀)} ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) × {0}))
115		xpundir 5514	. . . . . . . . . . . . . . . 16 ⊢ (({((2^nd ‘(1^st ‘𝑇))‘𝑀)} ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) × {0}) = (({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {0}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))
116	114, 115	syl6eq 2849	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}) = (({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {0}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
117	116	uneq2d 4066	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {0}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
118		un12 4070	. . . . . . . . . . . . . 14 ⊢ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {0}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) = (({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
119	117, 118	syl6eq 2849	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})) = (({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
120	119	fveq1d 6547	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = ((({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
121	120	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = ((({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
122		fnconstg 6442	. . . . . . . . . . . . . . . . 17 ⊢ (0 ∈ V → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
123	36, 122	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))
124	35, 123	pm3.2i 471	. . . . . . . . . . . . . . 15 ⊢ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∧ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
125		imain 6316	. . . . . . . . . . . . . . . . 17 ⊢ (Fun ^◡(2^nd ‘(1^st ‘𝑇)) → ((2^nd ‘(1^st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
126	42, 125	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
127	75	zred 11941	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀 − 1) ∈ ℝ)
128		peano2re 10666	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
129	47, 128	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀 + 1) ∈ ℝ)
130	47	ltp1d 11424	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
131	127, 47, 129, 48, 130	lttrd 10654	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 − 1) < (𝑀 + 1))
132		fzdisj 12788	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 − 1) < (𝑀 + 1) → ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁)) = ∅)
133	131, 132	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁)) = ∅)
134	133	imaeq2d 5813	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑇)) “ ∅))
135	134, 52	syl6eq 2849	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = ∅)
136	126, 135	eqtr3d 2835	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅)
137		fnun 6340	. . . . . . . . . . . . . . 15 ⊢ ((((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∧ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) ∧ (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
138	124, 136, 137	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
139		imaundi 5891	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
140		imadif 6315	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun ^◡(2^nd ‘(1^st ‘𝑇)) → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑁) ∖ {𝑀})) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑇)) “ {𝑀})))
141	42, 140	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑁) ∖ {𝑀})) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑇)) “ {𝑀})))
142		fzsplit 12787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
143	26, 142	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
144	143	difeq1d 4025	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1...𝑁) ∖ {𝑀}) = (((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∖ {𝑀}))
145		difundir 4183	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∖ {𝑀}) = (((1...𝑀) ∖ {𝑀}) ∪ (((𝑀 + 1)...𝑁) ∖ {𝑀}))
146		fzsplit2 12786	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑀 − 1) + 1) ∈ (ℤ_≥‘1) ∧ 𝑀 ∈ (ℤ_≥‘(𝑀 − 1))) → (1...𝑀) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀)))
147	73, 79, 146	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (1...𝑀) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀)))
148	59	oveq1d 7038	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑀) = (𝑀...𝑀))
149		fzsn 12803	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
150	46, 149	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑀...𝑀) = {𝑀})
151	148, 150	eqtrd 2833	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑀) = {𝑀})
152	151	uneq2d 4066	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀)) = ((1...(𝑀 − 1)) ∪ {𝑀}))
153	147, 152	eqtrd 2833	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1...𝑀) = ((1...(𝑀 − 1)) ∪ {𝑀}))
154	153	difeq1d 4025	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1...𝑀) ∖ {𝑀}) = (((1...(𝑀 − 1)) ∪ {𝑀}) ∖ {𝑀}))
155		difun2 4349	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...(𝑀 − 1)) ∪ {𝑀}) ∖ {𝑀}) = ((1...(𝑀 − 1)) ∖ {𝑀})
156	127, 47	ltnled 10640	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝑀 − 1) < 𝑀 ↔ ¬ 𝑀 ≤ (𝑀 − 1)))
157	48, 156	mpbid 233	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ¬ 𝑀 ≤ (𝑀 − 1))
158		elfzle2 12765	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 ∈ (1...(𝑀 − 1)) → 𝑀 ≤ (𝑀 − 1))
159	157, 158	nsyl 142	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ¬ 𝑀 ∈ (1...(𝑀 − 1)))
160		difsn 4644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑀 ∈ (1...(𝑀 − 1)) → ((1...(𝑀 − 1)) ∖ {𝑀}) = (1...(𝑀 − 1)))
161	159, 160	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((1...(𝑀 − 1)) ∖ {𝑀}) = (1...(𝑀 − 1)))
162	155, 161	syl5eq 2845	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((1...(𝑀 − 1)) ∪ {𝑀}) ∖ {𝑀}) = (1...(𝑀 − 1)))
163	154, 162	eqtrd 2833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((1...𝑀) ∖ {𝑀}) = (1...(𝑀 − 1)))
164	47, 129	ltnled 10640	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
165	130, 164	mpbid 233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
166		elfzle1 12764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 ∈ ((𝑀 + 1)...𝑁) → (𝑀 + 1) ≤ 𝑀)
167	165, 166	nsyl 142	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 𝑀 ∈ ((𝑀 + 1)...𝑁))
168		difsn 4644	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝑀 ∈ ((𝑀 + 1)...𝑁) → (((𝑀 + 1)...𝑁) ∖ {𝑀}) = ((𝑀 + 1)...𝑁))
169	167, 168	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((𝑀 + 1)...𝑁) ∖ {𝑀}) = ((𝑀 + 1)...𝑁))
170	163, 169	uneq12d 4067	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((1...𝑀) ∖ {𝑀}) ∪ (((𝑀 + 1)...𝑁) ∖ {𝑀})) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁)))
171	145, 170	syl5eq 2845	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∖ {𝑀}) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁)))
172	144, 171	eqtrd 2833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1...𝑁) ∖ {𝑀}) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁)))
173	172	imaeq2d 5813	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑁) ∖ {𝑀})) = ((2^nd ‘(1^st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))))
174	111	eqcomd 2803	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ {𝑀}) = {((2^nd ‘(1^st ‘𝑇))‘𝑀)})
175	96, 174	difeq12d 4027	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) ∖ ((2^nd ‘(1^st ‘𝑇)) “ {𝑀})) = ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}))
176	141, 173, 175	3eqtr3d 2841	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) = ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}))
177	139, 176	syl5eqr 2847	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}))
178	177	fneq2d 6324	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) ↔ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)})))
179	138, 178	mpbid 233	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}))
180		eldifsn 4632	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}) ↔ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)))
181	180	biimpri 229	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)) → 𝑛 ∈ ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}))
182	181	ancoms 459	. . . . . . . . . . . . 13 ⊢ ((𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}))
183		disjdif 4341	. . . . . . . . . . . . . 14 ⊢ ({((2^nd ‘(1^st ‘𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)})) = ∅
184		fnconstg 6442	. . . . . . . . . . . . . . . 16 ⊢ (0 ∈ V → ({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {0}) Fn {((2^nd ‘(1^st ‘𝑇))‘𝑀)})
185	36, 184	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {0}) Fn {((2^nd ‘(1^st ‘𝑇))‘𝑀)}
186		fvun2 6629	. . . . . . . . . . . . . . 15 ⊢ ((({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {0}) Fn {((2^nd ‘(1^st ‘𝑇))‘𝑀)} ∧ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}) ∧ (({((2^nd ‘(1^st ‘𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)})) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}))) → ((({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
187	185, 186	mp3an1 1440	. . . . . . . . . . . . . 14 ⊢ ((((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}) ∧ (({((2^nd ‘(1^st ‘𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)})) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}))) → ((({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
188	183, 187	mpanr1 699	. . . . . . . . . . . . 13 ⊢ ((((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}) ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)})) → ((({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
189	179, 182, 188	syl2an 595	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∧ 𝑛 ∈ (1...𝑁))) → ((({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
190	189	anassrs 468	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → ((({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
191	121, 190	eqtrd 2833	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
192	32, 100, 101, 101, 102, 103, 191	ofval 7283	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1^st ‘(1^st ‘𝑇))‘𝑛) + (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)))
193		fnconstg 6442	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ V → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)))
194	33, 193	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))
195	194, 123	pm3.2i 471	. . . . . . . . . . . . 13 ⊢ ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
196		imain 6316	. . . . . . . . . . . . . . 15 ⊢ (Fun ^◡(2^nd ‘(1^st ‘𝑇)) → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
197	42, 196	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
198		fzdisj 12788	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
199	130, 198	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
200	199	imaeq2d 5813	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2^nd ‘(1^st ‘𝑇)) “ ∅))
201	200, 52	syl6eq 2849	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
202	197, 201	eqtr3d 2835	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅)
203		fnun 6340	. . . . . . . . . . . . 13 ⊢ ((((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) ∧ (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
204	195, 202, 203	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
205	143	imaeq2d 5813	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
206		imaundi 5891	. . . . . . . . . . . . . . 15 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
207	205, 206	syl6eq 2849	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑁)) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))))
208	207, 96	eqtr3d 2835	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
209	208	fneq2d 6324	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∪ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) ↔ ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁)))
210	204, 209	mpbid 233	. . . . . . . . . . 11 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
211	210	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
212		imaundi 5891	. . . . . . . . . . . . . . . . . 18 ⊢ ((2^nd ‘(1^st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ {𝑀})) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^nd ‘(1^st ‘𝑇)) “ {𝑀}))
213	153	imaeq2d 5813	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) = ((2^nd ‘(1^st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ {𝑀})))
214	111	uneq2d 4066	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^nd ‘(1^st ‘𝑇)) “ {𝑀})))
215	212, 213, 214	3eqtr4a 2859	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}))
216	215	xpeq1d 5479	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}) × {1}))
217		xpundir 5514	. . . . . . . . . . . . . . . 16 ⊢ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}) × {1}) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ ({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1}))
218	216, 217	syl6eq 2849	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ ({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1})))
219	218	uneq1d 4065	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ ({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1})) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
220		un23 4071	. . . . . . . . . . . . . . 15 ⊢ (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ ({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1})) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) ∪ ({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1}))
221	220	equncomi 4058	. . . . . . . . . . . . . 14 ⊢ (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ ({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1})) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
222	219, 221	syl6eq 2849	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
223	222	fveq1d 6547	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = ((({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
224	223	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = ((({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
225		fnconstg 6442	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ V → ({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1}) Fn {((2^nd ‘(1^st ‘𝑇))‘𝑀)})
226	33, 225	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1}) Fn {((2^nd ‘(1^st ‘𝑇))‘𝑀)}
227		fvun2 6629	. . . . . . . . . . . . . . 15 ⊢ ((({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1}) Fn {((2^nd ‘(1^st ‘𝑇))‘𝑀)} ∧ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}) ∧ (({((2^nd ‘(1^st ‘𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)})) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}))) → ((({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
228	226, 227	mp3an1 1440	. . . . . . . . . . . . . 14 ⊢ ((((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}) ∧ (({((2^nd ‘(1^st ‘𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)})) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}))) → ((({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
229	183, 228	mpanr1 699	. . . . . . . . . . . . 13 ⊢ ((((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)}) ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2^nd ‘(1^st ‘𝑇))‘𝑀)})) → ((({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
230	179, 182, 229	syl2an 595	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∧ 𝑛 ∈ (1...𝑁))) → ((({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
231	230	anassrs 468	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → ((({((2^nd ‘(1^st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
232	224, 231	eqtrd 2833	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
233	32, 211, 101, 101, 102, 103, 232	ofval 7283	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((1^st ‘(1^st ‘𝑇))‘𝑛) + (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)))
234	192, 233	eqtr4d 2836	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
235	234	an32s 648	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀)) → (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
236	235	anasss 467	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀))) → (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
237		fveq2 6545	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → (2^nd ‘𝑡) = (2^nd ‘𝑇))
238	237	breq2d 4980	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑇 → (𝑦 < (2^nd ‘𝑡) ↔ 𝑦 < (2^nd ‘𝑇)))
239	238	ifbid 4409	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑇 → if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)))
240	239	csbeq1d 3821	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
241		2fveq3 6550	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑇 → (1^st ‘(1^st ‘𝑡)) = (1^st ‘(1^st ‘𝑇)))
242		2fveq3 6550	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑇 → (2^nd ‘(1^st ‘𝑡)) = (2^nd ‘(1^st ‘𝑇)))
243	242	imaeq1d 5812	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)))
244	243	xpeq1d 5479	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}))
245	242	imaeq1d 5812	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → ((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)))
246	245	xpeq1d 5479	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
247	244, 246	uneq12d 4067	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑇 → ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
248	241, 247	oveq12d 7041	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑇 → ((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
249	248	csbeq2dv 3824	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
250	240, 249	eqtrd 2833	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
251	250	mpteq2dv 5063	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
252	251	eqeq2d 2807	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑡)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
253	252, 3	elrab2 3624	. . . . . . . . . . 11 ⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
254	253	simprbi 497	. . . . . . . . . 10 ⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
255	1, 254	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
256		breq1 4971	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑀 − 2) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑀 − 2) < (2^nd ‘𝑇)))
257	256	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑀 − 2) < (2^nd ‘𝑇)))
258		oveq1 7030	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑀 − 2) → (𝑦 + 1) = ((𝑀 − 2) + 1))
259		sub1m1 11743	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) − 1) = (𝑀 − 2))
260	57, 259	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 − 1) − 1) = (𝑀 − 2))
261	260	oveq1d 7038	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑀 − 1) − 1) + 1) = ((𝑀 − 2) + 1))
262	75	zcnd 11942	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 − 1) ∈ ℂ)
263		npcan1 10919	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 − 1) ∈ ℂ → (((𝑀 − 1) − 1) + 1) = (𝑀 − 1))
264	262, 263	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑀 − 1) − 1) + 1) = (𝑀 − 1))
265	261, 264	eqtr3d 2835	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀 − 2) + 1) = (𝑀 − 1))
266	258, 265	sylan9eqr 2855	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → (𝑦 + 1) = (𝑀 − 1))
267	257, 266	ifbieq2d 4412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = if((𝑀 − 2) < (2^nd ‘𝑇), 𝑦, (𝑀 − 1)))
268	18	nncnd 11508	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℂ)
269		add1p1 11742	. . . . . . . . . . . . . . . . 17 ⊢ ((2^nd ‘𝑇) ∈ ℂ → (((2^nd ‘𝑇) + 1) + 1) = ((2^nd ‘𝑇) + 2))
270	268, 269	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((2^nd ‘𝑇) + 1) + 1) = ((2^nd ‘𝑇) + 2))
271	270, 67	eqbrtrrd 4992	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2^nd ‘𝑇) + 2) ≤ 𝑀)
272	18	nnred 11507	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2^nd ‘𝑇) ∈ ℝ)
273		2re 11565	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
274		leaddsub 10970	. . . . . . . . . . . . . . . . . 18 ⊢ (((2^nd ‘𝑇) ∈ ℝ ∧ 2 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((2^nd ‘𝑇) + 2) ≤ 𝑀 ↔ (2^nd ‘𝑇) ≤ (𝑀 − 2)))
275	273, 274	mp3an2 1441	. . . . . . . . . . . . . . . . 17 ⊢ (((2^nd ‘𝑇) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((2^nd ‘𝑇) + 2) ≤ 𝑀 ↔ (2^nd ‘𝑇) ≤ (𝑀 − 2)))
276	272, 47, 275	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((2^nd ‘𝑇) + 2) ≤ 𝑀 ↔ (2^nd ‘𝑇) ≤ (𝑀 − 2)))
277	60, 47	posdifd 11081	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (1 < 𝑀 ↔ 0 < (𝑀 − 1)))
278	68, 277	mpbid 233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 0 < (𝑀 − 1))
279		elnnz 11845	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 − 1) ∈ ℕ ↔ ((𝑀 − 1) ∈ ℤ ∧ 0 < (𝑀 − 1)))
280	75, 278, 279	sylanbrc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀 − 1) ∈ ℕ)
281		nnm1nn0 11792	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 − 1) ∈ ℕ → ((𝑀 − 1) − 1) ∈ ℕ₀)
282	280, 281	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑀 − 1) − 1) ∈ ℕ₀)
283	260, 282	eqeltrrd 2886	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 − 2) ∈ ℕ₀)
284	283	nn0red 11810	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 − 2) ∈ ℝ)
285	272, 284	lenltd 10639	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2^nd ‘𝑇) ≤ (𝑀 − 2) ↔ ¬ (𝑀 − 2) < (2^nd ‘𝑇)))
286	276, 285	bitrd 280	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2^nd ‘𝑇) + 2) ≤ 𝑀 ↔ ¬ (𝑀 − 2) < (2^nd ‘𝑇)))
287	271, 286	mpbid 233	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (𝑀 − 2) < (2^nd ‘𝑇))
288	287	iffalsed 4398	. . . . . . . . . . . . 13 ⊢ (𝜑 → if((𝑀 − 2) < (2^nd ‘𝑇), 𝑦, (𝑀 − 1)) = (𝑀 − 1))
289	288	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → if((𝑀 − 2) < (2^nd ‘𝑇), 𝑦, (𝑀 − 1)) = (𝑀 − 1))
290	267, 289	eqtrd 2833	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = (𝑀 − 1))
291	290	csbeq1d 3821	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑀 − 1) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
292		oveq2 7031	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑀 − 1) → (1...𝑗) = (1...(𝑀 − 1)))
293	292	imaeq2d 5813	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑀 − 1) → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))))
294	293	xpeq1d 5479	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑀 − 1) → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}))
295	294	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}))
296		oveq1 7030	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑀 − 1) → (𝑗 + 1) = ((𝑀 − 1) + 1))
297	296, 59	sylan9eqr 2855	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑗 + 1) = 𝑀)
298	297	oveq1d 7038	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑗 + 1)...𝑁) = (𝑀...𝑁))
299	298	imaeq2d 5813	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)))
300	299	xpeq1d 5479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}))
301	295, 300	uneq12d 4067	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})))
302	301	oveq2d 7039	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}))))
303	75, 302	csbied 3850	. . . . . . . . . . 11 ⊢ (𝜑 → ⦋(𝑀 − 1) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}))))
304	303	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → ⦋(𝑀 − 1) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}))))
305	291, 304	eqtrd 2833	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}))))
306		poimir.0	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ)
307		nnm1nn0 11792	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
308	306, 307	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
309	306	nnred 11507	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℝ)
310	47	lem1d 11427	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀 − 1) ≤ 𝑀)
311		elfzle2 12765	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ((((2^nd ‘𝑇) + 1) + 1)...𝑁) → 𝑀 ≤ 𝑁)
312	25, 311	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ≤ 𝑁)
313	127, 47, 309, 310, 312	letrd 10650	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 − 1) ≤ 𝑁)
314	127, 309, 60, 313	lesub1dd 11110	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑀 − 1) − 1) ≤ (𝑁 − 1))
315	260, 314	eqbrtrrd 4992	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 − 2) ≤ (𝑁 − 1))
316		elfz2nn0 12852	. . . . . . . . . 10 ⊢ ((𝑀 − 2) ∈ (0...(𝑁 − 1)) ↔ ((𝑀 − 2) ∈ ℕ₀ ∧ (𝑁 − 1) ∈ ℕ₀ ∧ (𝑀 − 2) ≤ (𝑁 − 1)))
317	283, 308, 315, 316	syl3anbrc 1336	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 − 2) ∈ (0...(𝑁 − 1)))
318		ovexd 7057	. . . . . . . . 9 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}))) ∈ V)
319	255, 305, 317, 318	fvmptd 6648	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘(𝑀 − 2)) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}))))
320	319	fveq1d 6547	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘(𝑀 − 2))‘𝑛) = (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛))
321	320	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 2))‘𝑛) = (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛))
322		breq1 4971	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑀 − 1) < (2^nd ‘𝑇)))
323	322	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → (𝑦 < (2^nd ‘𝑇) ↔ (𝑀 − 1) < (2^nd ‘𝑇)))
324		oveq1 7030	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 + 1) = ((𝑀 − 1) + 1))
325	324, 59	sylan9eqr 2855	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → (𝑦 + 1) = 𝑀)
326	323, 325	ifbieq2d 4412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < (2^nd ‘𝑇), 𝑦, 𝑀))
327	62	lep1d 11425	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ≤ (((2^nd ‘𝑇) + 1) + 1))
328	62, 61, 47, 327, 67	letrd 10650	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2^nd ‘𝑇) + 1) ≤ 𝑀)
329		1re 10494	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ
330		leaddsub 10970	. . . . . . . . . . . . . . . . . 18 ⊢ (((2^nd ‘𝑇) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((2^nd ‘𝑇) + 1) ≤ 𝑀 ↔ (2^nd ‘𝑇) ≤ (𝑀 − 1)))
331	329, 330	mp3an2 1441	. . . . . . . . . . . . . . . . 17 ⊢ (((2^nd ‘𝑇) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((2^nd ‘𝑇) + 1) ≤ 𝑀 ↔ (2^nd ‘𝑇) ≤ (𝑀 − 1)))
332	272, 47, 331	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((2^nd ‘𝑇) + 1) ≤ 𝑀 ↔ (2^nd ‘𝑇) ≤ (𝑀 − 1)))
333	272, 127	lenltd 10639	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2^nd ‘𝑇) ≤ (𝑀 − 1) ↔ ¬ (𝑀 − 1) < (2^nd ‘𝑇)))
334	332, 333	bitrd 280	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2^nd ‘𝑇) + 1) ≤ 𝑀 ↔ ¬ (𝑀 − 1) < (2^nd ‘𝑇)))
335	328, 334	mpbid 233	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (𝑀 − 1) < (2^nd ‘𝑇))
336	335	iffalsed 4398	. . . . . . . . . . . . 13 ⊢ (𝜑 → if((𝑀 − 1) < (2^nd ‘𝑇), 𝑦, 𝑀) = 𝑀)
337	336	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if((𝑀 − 1) < (2^nd ‘𝑇), 𝑦, 𝑀) = 𝑀)
338	326, 337	eqtrd 2833	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑀)
339	338	csbeq1d 3821	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑀 / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
340		oveq2 7031	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → (1...𝑗) = (1...𝑀))
341	340	imaeq2d 5813	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) = ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)))
342	341	xpeq1d 5479	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}))
343		oveq1 7030	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑀 → (𝑗 + 1) = (𝑀 + 1))
344	343	oveq1d 7038	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑀 → ((𝑗 + 1)...𝑁) = ((𝑀 + 1)...𝑁))
345	344	imaeq2d 5813	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑀 → ((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))
346	345	xpeq1d 5479	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑀 → (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))
347	342, 346	uneq12d 4067	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑀 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
348	347	oveq2d 7039	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑀 → ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
349	348	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 = 𝑀) → ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
350	25, 349	csbied 3850	. . . . . . . . . . 11 ⊢ (𝜑 → ⦋𝑀 / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
351	350	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋𝑀 / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
352	339, 351	eqtrd 2833	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < (2^nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
353	280	nnnn0d 11809	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 − 1) ∈ ℕ₀)
354	47, 309, 60, 312	lesub1dd 11110	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 − 1) ≤ (𝑁 − 1))
355		elfz2nn0 12852	. . . . . . . . . 10 ⊢ ((𝑀 − 1) ∈ (0...(𝑁 − 1)) ↔ ((𝑀 − 1) ∈ ℕ₀ ∧ (𝑁 − 1) ∈ ℕ₀ ∧ (𝑀 − 1) ≤ (𝑁 − 1)))
356	353, 308, 354, 355	syl3anbrc 1336	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 − 1) ∈ (0...(𝑁 − 1)))
357		ovexd 7057	. . . . . . . . 9 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
358	255, 352, 356, 357	fvmptd 6648	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘(𝑀 − 1)) = ((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
359	358	fveq1d 6547	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑛) = (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
360	359	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 1))‘𝑛) = (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
361	236, 321, 360	3eqtr4d 2843	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 2))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑛))
362	361	expr 457	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 ≠ ((2^nd ‘(1^st ‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑛)))
363	362	necon1d 3008	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛) → 𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑀)))
364		elmapi 8285	. . . . . . . . . . 11 ⊢ ((1^st ‘(1^st ‘𝑇)) ∈ ((0..^𝐾) ↑_𝑚 (1...𝑁)) → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
365	29, 364	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘(1^st ‘𝑇)):(1...𝑁)⟶(0..^𝐾))
366	365, 27	ffvelrnd 6724	. . . . . . . . 9 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) ∈ (0..^𝐾))
367		elfzonn0 12936	. . . . . . . . 9 ⊢ (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) ∈ (0..^𝐾) → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) ∈ ℕ₀)
368	366, 367	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) ∈ ℕ₀)
369	368	nn0red 11810	. . . . . . 7 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) ∈ ℝ)
370	369	ltp1d 11424	. . . . . . 7 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) < (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) + 1))
371	369, 370	ltned 10629	. . . . . 6 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) ≠ (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) + 1))
372	319	fveq1d 6547	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘(𝑀 − 2))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)))
373		ovexd 7057	. . . . . . . . 9 ⊢ (𝜑 → (1...𝑁) ∈ V)
374		eqidd 2798	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∈ (1...𝑁)) → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)))
375		fzss1 12800	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ_≥‘1) → (𝑀...𝑁) ⊆ (1...𝑁))
376	72, 375	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀...𝑁) ⊆ (1...𝑁))
377		eluzfz1 12768	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))
378	83, 377	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁))
379		fnfvima 6867	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁) ∧ (𝑀...𝑁) ⊆ (1...𝑁) ∧ 𝑀 ∈ (𝑀...𝑁)) → ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∈ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)))
380	109, 376, 378, 379	syl3anc 1364	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∈ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)))
381		fvun2 6629	. . . . . . . . . . . . 13 ⊢ (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∧ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) ∧ ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁))) = ∅ ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∈ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = ((((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2^nd ‘(1^st ‘𝑇))‘𝑀)))
382	35, 38, 381	mp3an12 1443	. . . . . . . . . . . 12 ⊢ (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁))) = ∅ ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∈ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = ((((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2^nd ‘(1^st ‘𝑇))‘𝑀)))
383	54, 380, 382	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = ((((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2^nd ‘(1^st ‘𝑇))‘𝑀)))
384	36	fvconst2 6840	. . . . . . . . . . . 12 ⊢ (((2^nd ‘(1^st ‘𝑇))‘𝑀) ∈ ((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) → ((((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = 0)
385	380, 384	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = 0)
386	383, 385	eqtrd 2833	. . . . . . . . . 10 ⊢ (𝜑 → (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = 0)
387	386	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∈ (1...𝑁)) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = 0)
388	31, 99, 373, 373, 102, 374, 387	ofval 7283	. . . . . . . 8 ⊢ ((𝜑 ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) + 0))
389	27, 388	mpdan 683	. . . . . . 7 ⊢ (𝜑 → (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) + 0))
390	368	nn0cnd 11811	. . . . . . . 8 ⊢ (𝜑 → ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) ∈ ℂ)
391	390	addid1d 10693	. . . . . . 7 ⊢ (𝜑 → (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) + 0) = ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)))
392	372, 389, 391	3eqtrd 2837	. . . . . 6 ⊢ (𝜑 → ((𝐹‘(𝑀 − 2))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = ((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)))
393	358	fveq1d 6547	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)))
394		fzss2 12801	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (1...𝑀) ⊆ (1...𝑁))
395	83, 394	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑀) ⊆ (1...𝑁))
396		elfz1end 12791	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈ (1...𝑀))
397	71, 396	sylib 219	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ (1...𝑀))
398		fnfvima 6867	. . . . . . . . . . . . 13 ⊢ (((2^nd ‘(1^st ‘𝑇)) Fn (1...𝑁) ∧ (1...𝑀) ⊆ (1...𝑁) ∧ 𝑀 ∈ (1...𝑀)) → ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)))
399	109, 395, 397, 398	syl3anc 1364	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)))
400		fvun1 6628	. . . . . . . . . . . . 13 ⊢ (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∧ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) ∧ ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘((2^nd ‘(1^st ‘𝑇))‘𝑀)))
401	194, 123, 400	mp3an12 1443	. . . . . . . . . . . 12 ⊢ (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) ∩ ((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀))) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘((2^nd ‘(1^st ‘𝑇))‘𝑀)))
402	202, 399, 401	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘((2^nd ‘(1^st ‘𝑇))‘𝑀)))
403	33	fvconst2 6840	. . . . . . . . . . . 12 ⊢ (((2^nd ‘(1^st ‘𝑇))‘𝑀) ∈ ((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = 1)
404	399, 403	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1})‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = 1)
405	402, 404	eqtrd 2833	. . . . . . . . . 10 ⊢ (𝜑 → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = 1)
406	405	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∈ (1...𝑁)) → (((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = 1)
407	31, 210, 373, 373, 102, 374, 406	ofval 7283	. . . . . . . 8 ⊢ ((𝜑 ∧ ((2^nd ‘(1^st ‘𝑇))‘𝑀) ∈ (1...𝑁)) → (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) + 1))
408	27, 407	mpdan 683	. . . . . . 7 ⊢ (𝜑 → (((1^st ‘(1^st ‘𝑇)) ∘_𝑓 + ((((2^nd ‘(1^st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^nd ‘(1^st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) + 1))
409	393, 408	eqtrd 2833	. . . . . 6 ⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) = (((1^st ‘(1^st ‘𝑇))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) + 1))
410	371, 392, 409	3netr4d 3063	. . . . 5 ⊢ (𝜑 → ((𝐹‘(𝑀 − 2))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) ≠ ((𝐹‘(𝑀 − 1))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)))
411		fveq2 6545	. . . . . 6 ⊢ (𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) = ((𝐹‘(𝑀 − 2))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)))
412		fveq2 6545	. . . . . 6 ⊢ (𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)))
413	411, 412	neeq12d 3047	. . . . 5 ⊢ (𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑀) → (((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛) ↔ ((𝐹‘(𝑀 − 2))‘((2^nd ‘(1^st ‘𝑇))‘𝑀)) ≠ ((𝐹‘(𝑀 − 1))‘((2^nd ‘(1^st ‘𝑇))‘𝑀))))
414	410, 413	syl5ibrcom 248	. . . 4 ⊢ (𝜑 → (𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)))
415	414	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)))
416	363, 415	impbid 213	. 2 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛) ↔ 𝑛 = ((2^nd ‘(1^st ‘𝑇))‘𝑀)))
417	27, 416	riota5 7010	1 ⊢ (𝜑 → (℩𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)) = ((2^nd ‘(1^st ‘𝑇))‘𝑀))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1525 ∈ wcel 2083 {cab 2777 ≠ wne 2986 {crab 3111 Vcvv 3440 ⦋csb 3817 ∖ cdif 3862 ∪ cun 3863 ∩ cin 3864 ⊆ wss 3865 ∅c0 4217 ifcif 4387 {csn 4478 class class class wbr 4968 ↦ cmpt 5047 × cxp 5448 ^◡ccnv 5449 “ cima 5453 Fun wfun 6226 Fn wfn 6227 ⟶wf 6228 –onto→wfo 6230 –1-1-onto→wf1o 6231 ‘cfv 6232 ℩crio 6983 (class class class)co 7023 ∘_𝑓 cof 7272 1^st c1st 7550 2^nd c2nd 7551 ↑_𝑚 cmap 8263 ℂcc 10388 ℝcr 10389 0cc0 10390 1c1 10391 + caddc 10393 < clt 10528 ≤ cle 10529 − cmin 10723 ℕcn 11492 2c2 11546 ℕ₀cn0 11751 ℤcz 11835 ℤ_≥cuz 12097 ...cfz 12746 ..^cfzo 12887

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-rep 5088 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 ax-cnex 10446 ax-resscn 10447 ax-1cn 10448 ax-icn 10449 ax-addcl 10450 ax-addrcl 10451 ax-mulcl 10452 ax-mulrcl 10453 ax-mulcom 10454 ax-addass 10455 ax-mulass 10456 ax-distr 10457 ax-i2m1 10458 ax-1ne0 10459 ax-1rid 10460 ax-rnegex 10461 ax-rrecex 10462 ax-cnre 10463 ax-pre-lttri 10464 ax-pre-lttrn 10465 ax-pre-ltadd 10466 ax-pre-mulgt0 10467

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-nel 3093 df-ral 3112 df-rex 3113 df-reu 3114 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-pss 3882 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-tp 4483 df-op 4485 df-uni 4752 df-iun 4833 df-br 4969 df-opab 5031 df-mpt 5048 df-tr 5071 df-id 5355 df-eprel 5360 df-po 5369 df-so 5370 df-fr 5409 df-we 5411 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-pred 6030 df-ord 6076 df-on 6077 df-lim 6078 df-suc 6079 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-riota 6984 df-ov 7026 df-oprab 7027 df-mpo 7028 df-of 7274 df-om 7444 df-1st 7552 df-2nd 7553 df-wrecs 7805 df-recs 7867 df-rdg 7905 df-er 8146 df-map 8265 df-en 8365 df-dom 8366 df-sdom 8367 df-pnf 10530 df-mnf 10531 df-xr 10532 df-ltxr 10533 df-le 10534 df-sub 10725 df-neg 10726 df-nn 11493 df-2 11554 df-n0 11752 df-z 11836 df-uz 12098 df-fz 12747 df-fzo 12888

This theorem is referenced by: poimirlem8 34452

W3C validator